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

Рассматриваются униформные системы взаимодействующих расширенных конечных автоматов, которые удобны для задания исходной спецификации телекоммуникационных систем, таких как кольцевые протоколы и телефонные сети. Цель работы – представить программный комплекс Automata Systems Verifier (ASV), предназначенный для анализа и верификации автоматных спецификаций. Он базируется на алгоритме трансляции систем автоматов в раскрашенные сети Петри (РСП), представленном и обоснованном в [4]. Для анализа РСП комплекс ASV использует систему CPN Tools [10], а для их верификации методом проверки моделей относительно свойств, заданных формулами мю-исчисления, он использует систему Petri Net Verifier [12]. Описано применение этого комплекса к верификации кольцевого RE-протокола и к исследованию взаимодействия функциональностей в телефонных сетях.