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

Вельдер Сергей Эдуардович, Шалыто Анатолий Абрамович

2009 , ТОМ 09, НОМЕР 6 ( НОЯБРЬ-ДЕКАБРЬ )

ISSN 2226-1494 (print), ISSN 2500-0373 (online)

Меню

Публикации

Главный редактор

НИКИФОРОВ
Владимир Олегович
д.т.н., профессор

Партнеры

УДК 004.4’242

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

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

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

Аннотация

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

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

верификация моделей, темпоральные логики, Model checking, автоматное программирование

This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License