Сборники трудов ИСП РАН


Инструмент для анализа поведения вполне структурированных систем переходов

Л.В. Дворянский (ВШЭ, Москва, Россия)
В.Е. Михайлов (ВШЭ, Москва, Россия)

Аннотация

Вполне структурированные системы переходов являются хорошо известным инструментом для доказательства разрешимости свойств покрываемости и ограниченности. Каждый год появляются новые формализмы, которые оказываются вполне структурированными системами переходов. Несмотря на большой объем теоретической работы, существует большая потребность в эмпирических изучении вполне структурированных систем переходов. В данной работе представлен инструмент для анализа таких систем. Мы предлагаем расширение высокоуровневого языка SETL для описания вполне-структурированных систем переходов. Это позволяет описывать новые формализмы близко к их формальному определению. Таким образом упрощается создание и изменение новых формализмов, а также осуществление анализа поведенческих свойств без большого объема программистских усилий. Это удобно, когда новый формализм находится в стадии изучения и разработки. Были реализованы два самых изученных алгоритма анализа поведения вполне структурированных систем переходов (обратный алгоритм и анализ конечных деревьев достижимости). Их производительность была измерена на моделях сетей Петри и систем с потерей сигналов. Разработанный инструмент может быть полезным при внедрении и тестировании методов анализа формализмов, которые оказываются вполне структурированными системами переходов.

Ключевые слова

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

Издание

Труды Института системного программирования РАН, том 29, вып. 4, 2017, стр. 175-190.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2017-29(4)-11

Полный текст статьи в формате pdf (на английском) Вернуться к содержанию тома