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

А. Н. Силаев, В. А. Саркисова, Е. А. Харченко

Московский политехнический университет, Россия

Аннотация: В работе выделяется специфичность проверки на соответствие заявленным требованиям алгоритмов, построенных на конечных автоматах. Предлагается облегченное инструментальное средство верификации автоматных алгоритмов по фрагментарному описанию входных цепочек. Программное решение имеет клиент-серверную архитектуру, где полные цепочки обрабатываются на стороне клиента, а неполные передаются на сервер. Возможны позитивный и негативный режимы проверки цепочек. В первом случае контекстом проверки является возможность реализации алгоритмом последовательности событий, во втором — невозможность. Для решения проблемы проверки цепочек с пропусками разработан оригинальный алгоритм, основанный на построении реконструирующего пропуски вспомогательного автомата. Назначение и работоспособность программного решения демонстрируются на известном литературном примере.

Ключевые слова: событийно-управляемая система, протокол, конечный автомат, грамматика, ANTLR

УДК: 004.4’2

Поступила в редакцию: 30.06.2025

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

•