Prosega/CPN: an extension of CPN Tools for automata-based analysis and system verification

Верификация и анализ распределенных систем являются чрезвычайно важными задачами, особенно сейчас, когда многие компьютерные системы реализуют критически важные сервисы. Для моделирования и верификации систем полезно сочетать разные методы анализа. В частности, это позволяет применять тот формализм и ту технику анализа, которые лучше подходят для того или иного компонента системы. Комбинация из раскрашенных сетей Петри (CPN, Coloured Petri Nets) и конечных автоматов представляет собой успешную формальную методику моделирования и верификации распределенных систем. В связи с этим в данной статье рассматривается инструмент Prosega/CPN (Protocol Sequence Generator and Analyzer), расширение CPN Tools для поддержки автоматного анализа и верификации. Инструмент реализует несколько функций, таких как генерация минимизированного детерминированного конечного автомата из графа достижимости (occurrence graph) раскрашенной сети Петри, генерация языка и сопоставление конечных автоматов. Это решение поддерживается функцией Simulator Extensions, развитие которой обусловлено необходимостью интеграции раскрашенных сетей Петри с другими формализмами. Инструмент предназначен для поддержки формальной методологии верификации коммуникационных протоколов; однако он может использоваться для верификации других систем, анализ которых включает сравнение моделей на разных уровнях абстракции, например, бизнес-стратегий и бизнес-процессов. В статье приведен подробный пример, в котором инструмент Prosega/CPN используется для анализа части спецификации службы управления соединениями MAC IEEE 802.16.