|
The application of coloured Petri nets to verification of distributed systems specified by message sequence charts
[Применение раскрашенных сетей Петри для верификации распределенных систем, специфицированных MSC-диаграммами]
S. A. Chernenok, V. A. Nepomniaschy A.P. Ershov Institute of Informatics Systems of the Siberian Branch of the RAS
Аннотация:
Язык диаграмм последовательностей сообщений (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.
Образец цитирования:
S. A. Chernenok, V. A. Nepomniaschy, “The application of coloured Petri nets to verification of distributed systems specified by message sequence charts”, Труды ИСП РАН, 27:3 (2015), 197–218
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/tisp146 https://www.mathnet.ru/rus/tisp/v27/i3/p197
|
Статистика просмотров: |
Страница аннотации: | 162 | PDF полного текста: | 65 | Список литературы: | 28 |
|