Кібернетика і Системний Аналіз
Міжнародний Науково-Теоретичний Журнал
Анотація. Представлено нову систему аналізу і верифікації Use Case Maps (UCM) специфікацій розфарбованих мереж Петрі та системи верифікації SPIN. Стандартизована нотація UCM зручний графічний засіб формального опису функціональних вимог. Описано алгоритми трансляції UCM-специфікацій в розфарбованій мережі Петрі, а також їх трансляцію у вихідну мову Promela системи SPIN. Зроблено висновок щодо оцінки складності отриманих розфарбованих мереж Петрі. Роботу наведених алгоритмів та інструментів показано на прикладі верифікації комунікаційного протоколу з локалізацією та виправленням помилок в початковій UCM-специфікації.
Ключові слова: верифікація, специфікація, розподілені системи, нотація Use Case Maps, розфарбовані мережі Петрі, система верифиікації SPIN.
Визовитин Николай Валерьевич,
младший нучный сотрудник Института систем информатики им. А.П. Ершова СО РАН, Новосибирск, Россия,
e-mail: vizovitin@gmail.com.
Непомнящий Валерий Александрович,
кандидат физ.-мат. наук, заведующий лабораторией Института систем информатики им. А.П. Ершова СО РАН, Новосибирск, Россия,
e-mail: vnep@iis.nsk.su.
Стененко Александр Александрович,
аспирант Института систем информатики им. А.П. Ершова СО РАН, Новосибирск, Россия,
e-mail: stirpar@gmail.com.
