Журнал
Научно-технический вестник информационных технологий, механики и оптики
УДК:004.4’242
Номер:8 (53)
Скачать PDF0 Кбайт
В статье описан разработанный авторами верификатор автоматных программ, созданных при помощи инструментального средства для поддержки автоматного программирования UniMod. При его использовании, в отличие от известных верификаторов, отсутствует необходимость описывать модель на входном языке верификатора. Требования к программе записываются на языке темпоральной логики линейного времени LTL (Linear Time Logic). При использовании такой логики верификация осуществляется за счет пересечения автомата-произведения модели и автомата Бюхи, построенного для отрицания LTL-формулы.