УДК 004.4’242

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

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



Аннотация

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


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

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



Creative Commons License

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License
Информация 2001-2024 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

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