Аннотация. Представлена новая система анализа и верификации 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.