Верификация UCM моделей с конструкциями управления сценариями с помощью раскрашенных сетей Петри

В статье представлен метод для анализа и верификации Use Case Maps (UCM) моделей с конструкциями управления сценариями, включающими защищенные компоненты и конструкции, служащие для обработки исключительных ситуаций. Анализ и верификация UCM моделей проводится с помощью раскрашенных сетей Петри (РСП) и верификатора SPIN. Описан алгоритм для трансляции конструкций управления сценариями из UCM в РСП. Алгоритм и процедура верификации продемонстрированы на примере сетевого протокола.