DOI: 10.17587/prin.13.155-167

УДК: 004.05

Автоматное программирование на базе системы моделирования и верификации Event-B

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

Представлен новый язык автоматного программирования, построенный расширением языка спецификаций Event-B. При разработке моделей в Event-B появляется возможность использования методов автоматного программирования в дополнение к популярному методу уточнений. Технология автоматного программирования на базе Event-B демонстрируется на примере задачи управления движением на мосту из руководства по системе Event-B. Предложено более простое решение с верификацией в инструменте Rodin. Эффективность методов верификации в Event-B подтверждена нахождением трех нетривиальных ошибок в приведенном решении.

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

Стр. 155—167