Методика верификации автоматных программ

Аннотация

Описывается разработанный верификатор автоматных программ, созданных при помощи инструментального средства для поддержки автоматного программирования UniMod. При его использовании отсутствует необходимость описывать модель на входном языке верификатора. Требования к программе записываются на языке темпоральной логики линейного времени.