УДК004.4’242

МЕТОДЫ ВЕРИФИКАЦИИ МОДЕЛЕЙ АВТОМАТНЫХ ПРОГРАММ

Вельдер С. Э., Шалыто А. А.



Аннотация

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


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

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

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

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