верификация моделей, темпоральные логики, Model checking, автоматное программирование " />
УДК004.4’242

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

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


Читать статью полностью 

Аннотация

 

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

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

 

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

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