- Об институте
- Инновации
- Структура
- Отдел "Архитектуры вычислительных систем"
- Отдел "Информационных систем"
- Отдел "Компиляторных технологий"
- Отдел "Системного программирования"
- Отдел "Системной интеграции и прикладных программных комплексов"
- Отдел "Теоретической информатики"
- Отдел "Технологий программирования"
- Ученый совет
- Диссертационный совет
- Центр верификации ОС Linux
- Исследовательский центр доверенного искусственного интеллекта
- Центр компетенции по параллельным и распределенным вычислениям
- Образование
- Издания
- Новости
- Лицензии
О верификации конечных параметризованных моделей распределенных программ.
Авторы
Захаров В.А., Булычев П.Е.
Аннотация
В настоящей работе введен и исследован новый класс параметризованных моделей распределенных программ. Модели представляют собой конечные размеченные системы переходов, в которых в качестве параметров используются булевы переменные. Благодаря этому открывается возможность компактного описания конечных семейств взаимодействующих процессов, в которых оценки событий в различных состояниях и осуществимость переходов между состояниями определенным образом согласованы между собой. Предложен символьный алгоритм верификации конечных параметризованных моделей программ для логики деревьев вычислений CTL, а также установлены оценки сложности рассматриваемой задачи.
Ключевые слова
программа, система переходов, спецификация, темпоральная логика, верификация, булева функция, OBDD, NP-полная задача.
Издание
Научные ведомости Белгородского государственного университета. Серия История, экономика, политология, информатика, 2009, том 9, № 11, с. 116-123.