Сравнение технологий автоматного программирования и Event-B

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