Платформа для динамической верификации гетерогенных свойств

[Константин Савенков]

Существует класс вычислительных систем, для которых полная статическая проверка правильности (в ходе их разработки) невозможна. В основном это связано с

1) возможность системы изменять свою конфигурацию в ходе работы (ad-hoc системы c беспроводной связью; системы с частичным обновлением ПО и конфигурации),

2) применением компонентов, для которых нет достаточных для статической верификации спецификации, а есть лишь описание интерфейсов (мульти-вендорные системы, компоненты которых разрабатываются различными компаниями),

3) сложный контекст работы системы (взаимодействие с реальным миром, Интернет).

До недавнего времени при разработке критически важных (safety-critical) систем подобные особенности и компоненты не использовались. Однако сейчас это уже не так, и если в каких-то областях этих проблем нет, то они появятся в ближайшем времени.

Для обеспечения надёжной работы таких систем необходимо использовать динамическую проверку правильности работы системы -- выполнять мониторинг поведения системы в реальном времени, оценивать соответствие наблюдаемого поведения спецификации, вовремя прогнозировать нарушение спецификации и предотвращать их. Существует достаточно много работ, посвящённых runtime monitoring и runtime verification, однако в них остаются открытыми следующие вопросы:

1) работа с разнообразными средствами описания свойств,

2) надёжность применяемых методов анализа и предотвращения сбоев,

3) эффективность алгоритмов анализа.

Этими вопросами и предполагается заняться в данной работе.