Сборники трудов ИСП РАН


Применение раскрашенных сетей Петри для верификации распределенных систем, специфицированных MSC-диаграммами

С.А. Черненок (ИСИ СО РАН, Новосибирск), В.А. Непомнящий (ИСИ СО РАН, Новосибирск)

Аннотация

Язык диаграмм последовательностей сообщений (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).

Ключевые слова

specification; translation; verification; distributed systems; communication protocols; message sequence charts; UML sequence diagrams; coloured Petri nets

Издание

Труды Института системного программирования РАН, том 27, вып. 3, 2015, стр. 197-218.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2015-27(3)-14

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома