Анализ и верификация MSC-диаграмм распределённых систем с помощью раскрашенных сетей Петри

Стандартный язык диаграмм последовательных сообщений MSC предназначен для описания сценариев взаимодействия объектов. Благодаря своей выразительности и простоте MSC-диаграммы широко применяются на практике на всех этапах проектирования и разработки программных систем. В частности, язык MSC используется для спецификации поведения в распределенных системах и коммуникационных протоколах. В работе рассматривается метод анализа и верификации диаграмм MSC и HMSC. Метод основывается на трансляции конструкций (H)MSC в раскрашенные сети Петри. Описываемые правила трансляции охватывают большинство конструкций стандарта, включая концепцию данных. Приводятся оценки размера сетей Петри, полученных в результате трансляции. Свойства построенных сетей анализируются и верифицируются с помощью известной системы CPN Tools и системы автоматической верификации на основе SPIN. Работоспособность данного метода продемонстрирована на примере.