О верификации конечных параметризованных моделей распределенных программ.

Авторы

Захаров В.А., Булычев П.Е.

Аннотация

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

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

программа, система переходов, спецификация, темпоральная логика, верификация, булева функция, OBDD, NP-полная задача.

Издание

Научные ведомости Белгородского государственного университета. Серия История, экономика, политология, информатика, 2009, том 9, № 11, с. 116-123.

Научная группа

Теоретическая информатика

Все публикации за 2009 год

Все публикации