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

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

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



Модел. и анализ информ. систем:
Год:
Том:
Выпуск:
Страница:
Найти






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


Модел. и анализ информ. систем, 2011, том 18, номер 4, страницы 144–156 (Mi mais205)  

Эта публикация цитируется в 1 научной статье (всего в 1 статье)

Верификация телекоммуникационных систем, специфицированных взаимодействующими конечными автоматами, с помощью раскрашенных сетей Петри

Д. М. Белоглазов, М. Ю. Машуков, В. А. Непомнящий

Институт систем информатики им. А.П. Ершова СО РАН

Аннотация: Рассматриваются униформные системы взаимодействующих расширенных конечных автоматов, которые удобны для задания исходной спецификации телекоммуникационных систем, таких как кольцевые протоколы и телефонные сети. Цель работы – представить программный комплекс Automata Systems Verifier (ASV), предназначенный для анализа и верификации автоматных спецификаций. Он базируется на алгоритме трансляции систем автоматов в раскрашенные сети Петри (РСП), представленном и обоснованном в [4]. Для анализа РСП комплекс ASV использует систему CPN Tools [10], а для их верификации методом проверки моделей относительно свойств, заданных формулами мю-исчисления, он использует систему Petri Net Verifier [12]. Описано применение этого комплекса к верификации кольцевого RE-протокола и к исследованию взаимодействия функциональностей в телефонных сетях.

Ключевые слова: телекоммуникационные системы, расширенные конечные автоматы, раскрашенные сети Петри, кольцевые протоколы, взаимодействие функциональностей, телефонные сети, верификация, метод проверки моделей.

Полный текст: PDF файл (471 kB)
Список литературы: PDF файл   HTML файл
Тип публикации: Статья
УДК: 519.681.3
Поступила в редакцию: 18.11.2011

Образец цитирования: Д. М. Белоглазов, М. Ю. Машуков, В. А. Непомнящий, “Верификация телекоммуникационных систем, специфицированных взаимодействующими конечными автоматами, с помощью раскрашенных сетей Петри”, Модел. и анализ информ. систем, 18:4 (2011), 144–156

Цитирование в формате AMSBIB
\RBibitem{BelMasNep11}
\by Д.~М.~Белоглазов, М.~Ю.~Машуков, В.~А.~Непомнящий
\paper Верификация телекоммуникационных систем, специфицированных взаимодействующими конечными автоматами, с помощью раскрашенных сетей Петри
\jour Модел. и анализ информ. систем
\yr 2011
\vol 18
\issue 4
\pages 144--156
\mathnet{http://mi.mathnet.ru/mais205}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais205
  • http://mi.mathnet.ru/rus/mais/v18/i4/p144

    ОТПРАВИТЬ: 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

    Эта публикация цитируется в следующих статьяx:
    1. И. С. Ануреев, С. Н. Баранов, Д. М. Белоглазов, Е. В. Бодин, П. Д. Дробинцев, А. В. Колчин, В. П. Котляров, А. А. Летичевский, А. А. Летичевский, В. А. Непомнящий, И. В. Никифоров, С. В. Потиенко, Л. В. Прийма, Б. В. Тютин, “Средства поддержки интегрированной технологии для анализа и верификации спецификаций телекоммуникационных приложений”, Тр. СПИИРАН, 26 (2013), 349–383  mathnet
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:250
    Полный текст:93
    Литература:28
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020