Abstract:
Работа выполнялась в лаборатории теоретического программирования
ИСИ СО РАН имени акад. А. П. Ершова. Она является развивает тему работы
бакалавры и посвящена созданию системы верификации раскрашенных сетей
Петри (РСП) и автоматных спецификаций, использующей систему SPIN. В
рамках данной работы был произведён анализ возможностей, предоставляемых
языками описания моделей (язык автоматных спецификаций, РСП и Promela),
были введены ограничения на входные языки, была разработана система
верификации, включающая транслятор из языка автоматных спецификаций в
РСП и транслятор из РСП в язык Promela. Работоспособность системы была
продемонстрирована её применением для верификации моделей
коммуникационных систем.
В ходе работы были получены следующие результаты:
1. Разработан алгоритм трансляции из РСП в Promela.
2. Создан транслятор, реализующий разработанный алгоритм.
3. Создан транслятор, реализующий алгоритм трансляции автоматных
спецификаций в РСП.
4. Произведена верификация моделей коммуникационных систем с
использованием созданных инструментов.
Текст работы содержит введение, четыре главы и заключение. В первой
главе определяются необходимые понятия. Вторая глава посвящена трансляции
РСП в язык Promela. Третья глава описывает трансляцию автоматных
спецификаций в РСП. Четвёртая глава содержит описание проведённых с
помощью разработанных средств экспериментов по верификации моделей
коммуникационных систем.
Объём работы — 53 страницы. Работа содержит 9 иллюстраций. Всего
использовано 20 источников информации.
