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

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

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



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






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


Модел. и анализ информ. систем, 2016, том 23, номер 6, страницы 688–702 (Mi mais533)  

Применение раскрашенных сетей Петри для верификации конструкций управления сценариями языка UCM

Н. В. Визовитин, В. А. Непомнящий, А. А. Стененко

Институт систем информатики им. А.П. Ершова СО РАН, проспект Академика Лаврентьева, 6, г. Новосибирск, 630090 Россия

Аннотация: В данной работе представлен метод анализа и верификации моделей Use Case Maps (UCM) с конструкциями управления сценариями — защищенными компонентами и конструкциями обработки ошибок. Анализ и верификация UCM моделей проводится с помощью раскрашенных сетей Петри (РСП) и верификатора SPIN. Приводятся описания алгоритмов трансляции UCM в РСП и РСП во входной язык Promela системы SPIN. Впервые представлены оценки для количества элементов результирующих РСП моделей в зависимости от количества элементов исходных UCM моделей с конструкциями управления сценариями, а также количества состояний Promela моделей. Представленный метод анализа и верификации демонстрируется на примере верификации программы обновления прошивки маршрутизатора.

Ключевые слова: верификация, трансляция, нотация Use Case Maps, раскрашенные сети Петри, верификатор SPIN, защищенный компонент, обработка ошибок.

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


DOI: https://doi.org/10.18255/1818-1015-2016-6-688-702

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

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

Тип публикации: Статья
УДК: 519.172
Поступила в редакцию: 15.03.2016

Образец цитирования: Н. В. Визовитин, В. А. Непомнящий, А. А. Стененко, “Применение раскрашенных сетей Петри для верификации конструкций управления сценариями языка UCM”, Модел. и анализ информ. систем, 23:6 (2016), 688–702

Цитирование в формате AMSBIB
\RBibitem{VizNepSte16}
\by Н.~В.~Визовитин, В.~А.~Непомнящий, А.~А.~Стененко
\paper Применение раскрашенных сетей Петри для верификации конструкций управления сценариями языка UCM
\jour Модел. и анализ информ. систем
\yr 2016
\vol 23
\issue 6
\pages 688--702
\mathnet{http://mi.mathnet.ru/mais533}
\crossref{https://doi.org/10.18255/1818-1015-2016-6-688-702}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=3596154}
\elib{http://elibrary.ru/item.asp?id=27517416}


Образцы ссылок на эту страницу:
  • http://mi.mathnet.ru/mais533
  • http://mi.mathnet.ru/rus/mais/v23/i6/p688

    ОТПРАВИТЬ: 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
  • Моделирование и анализ информационных систем
    Просмотров:
    Эта страница:126
    Полный текст:45
    Литература:20
     
    Обратная связь:
     Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2020