Например, Бобцов

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

Аннотация:

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

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

Статьи в номере