The application of coloured Petri nets to verification of distributed systems specified by message sequence charts

Язык диаграмм последовательностей сообщений (MSC-диаграмм) является сценарно-ориентированным языком спецификаций, который широко используется на этапе проектирования для описания взаимодействия компонент в распределенных системах. Однако, существующие методы и средства проверки корректности MSC-диаграмм недостаточно развиты. К их основным недостаткам относятся небольшой набор поддерживаемых конструкций MSC-диаграмм, ограничения на поведение элементов диаграмм и на набор анализируемых свойств. Данная статья описывает метод трансляции MSC-диаграмм в раскрашенные сети Петри (CPN), который используется для анализа и верификации свойств MSC-диаграмм. Метод трансляции состоит из трех основных этапов: построение внутреннего представления MSC-диаграммы в виде графа частичного порядка, обработка узлов графа и преобразование графа в CPN. Результатом трансляции является иерархическая раскрашенная сеть Петри в формате, совместимом с известной системой моделирования и анализа CPN Tools. Кроме элементов из основного стандарта MSC рассматриваются следующие конструкции MSC-диаграмм: элементы языка данных MSC (сообщения, локальные действия и условия с данными), элементы диаграмм взаимодействий стандарта UML (синхронные сообщения, комбинированные фрагменты) и конструкции композиционных MSC-диаграмм (частично-определенные сообщения). На основе этого метода трансляции реализован транслятор из MSC-диаграмм в CPN. Свойства результирующих CPN анализируются и верифицируются при помощи системы CPN Tools и верификатора CPN на основе системы SPIN. Если в результате верификации проверяемое свойство оказывается ложным и найден контрпример, то место ошибки может быть локализовано в исходной MSC-спецификации. Для этого на основе контрпримера генерируется трасса в MSC до места ошибки, представляющая собой последовательность событий диаграммы и состояний переменных каждого процесса. Применение метода трансляции и средств анализа и верификации продемонстрировано на примере сетевого протокола ABP (Alternating Bit Protocol).