УДК 004.4’242

РАЗРАБОТКА ВЕРИФИКАТОРА АВТОМАТНЫХ ПРОГРАММ

Егоров К. В., Шалыто А. А.



Аннотация

В статье описан разработанный авторами верификатор автоматных программ,  созданных при помощи инструментального средства для поддержки автоматного программирования UniMod. При его использовании, в отличие от известных верификаторов, отсутствует необходимость описывать модель на входном языке верификатора. Требования к программе записываются на языке темпоральной логики линейного времени LTL (Linear Time Logic). При использовании такой логики верификация осуществляется за счет пересечения автомата-произведения модели и автомата Бюхи, построенного для отрицания LTL-формулы.


Ключевые слова:

верификация программ,  верификация на моделях,  автоматное программирование,  автомат Бюхи

Информация 2001-2017 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

Яндекс.Метрика