DOI: 10.17587/prin.15.73-86

УДК: 004.05

Методы автоматного программирования для разработки и верификации систем управления

В. И. Шелехов¹,², канд. техн. наук, зав. лаб., vshel@iis.nsk.su, Э. Г. Тумуров¹, мл. науч. сотр., tumurov@iis.nsk.su
¹ Институт систем информатики им. А. П. Ершова СО РАН, Новосибирск,
² Новосибирский государственный университет

Автоматная композиция определяется как базисная языковая конструкция автоматного программирования. Включение автоматной композиции в произвольный язык программирования дает возможность реализации автоматных программ на этом языке. Детально определены методы спецификации и верификации реактивных систем. Методы автоматного программирования иллюстрируются на примере нетривиальной задачи управления движением автомобилями на мосту. Предложено более простое решение с верификацией в системах моделирования и верификации Event-B и Why3. Верификация в Why3 проводится на базе разработанной модели реактивной системы.

Ключевые слова: реактивная система, автоматное программирование, Event-B, Why3, уточнение (refinement), требования, дедуктивная верификация

Стр. 73–86

Ссылка для цитирования:
Шелехов В. И., Тумуров Э. Г. Методы автоматного программирования для разработки и верификации систем управления // Программная инженерия. 2024. Том 15, № 2. С. 73—86. DOI: 10.17587/prin.15.73-86.