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

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

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



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






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


Труды института системного программирования РАН, 2015, том 27, выпуск 3, страницы 197–218
DOI: https://doi.org/10.15514/ISPRAS-2015-27(3)-14
(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
Реферативные базы данных:
Тип публикации: Статья
Язык публикации: английский
Образец цитирования: 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{https://elibrary.ru/item.asp?id=23832943}
Образцы ссылок на эту страницу:
  • https://www.mathnet.ru/rus/tisp146
  • https://www.mathnet.ru/rus/tisp/v27/i3/p197
  • Citing articles in Google Scholar: Russian citations, English citations
    Related articles in Google Scholar: Russian articles, English articles
    Труды института системного программирования РАН
    Статистика просмотров:
    Страница аннотации:162
    PDF полного текста:65
    Список литературы:28
     
      Обратная связь:
     Пользовательское соглашение  Регистрация посетителей портала  Логотипы © Математический институт им. В. А. Стеклова РАН, 2024