RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ПАКЕТ AMSBIB
Общая информация
Последний выпуск
Архив

Поиск публикаций
Поиск ссылок

RSS
Последний выпуск
Текущие выпуски
Архивные выпуски
Что такое RSS



Труды ИСП РАН:
Год:
Том:
Выпуск:
Страница:
Найти






Персональный вход:
Логин:
Пароль:
Запомнить пароль
Войти
Забыли пароль?
Регистрация


Труды ИСП РАН, 2015, том 27, выпуск 3, страницы 197–218 (Mi tisp146)  

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.

Финансовая поддержка Номер гранта
Российский фонд фундаментальных исследований 14-07-00401


DOI: https://doi.org/10.15514/ISPRAS-2015-27(3)-14

Полный текст: PDF файл (412 kB)
Список литературы: PDF файл   HTML файл

Реферативные базы данных:

Тип публикации: Статья
Язык публикации: английский

Образец цитирования: 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

Цитирование в формате AMSBIB
\RBibitem{CheNep15}
\by S.~A.~Chernenok, V.~A.~Nepomniaschy
\paper The application of coloured Petri nets to verification of distributed systems specified by message sequence charts
\jour Труды ИСП РАН
\yr 2015
\vol 27
\issue 3
\pages 197--218
\mathnet{http://mi.mathnet.ru/tisp146}
\crossref{https://doi.org/10.15514/ISPRAS-2015-27(3)-14}
\elib{http://elibrary.ru/item.asp?id=23832943}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/tisp146
  • http://mi.mathnet.ru/rus/tisp/v27/i3/p197

    ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    Citing articles on Google Scholar: Russian citations, English citations
    Related articles on Google Scholar: Russian articles, English articles
  • Труды института системного программирования РАН
    Просмотров:
    Эта страница:89
    Полный текст:35
    Литература:16
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020