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

Abstract

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