Платформа для динамической верификации гетерогенных свойств
Добавлено: 08 дек 2009 02:17 pm
Существует класс вычислительных систем, для которых полная статическая проверка правильности (в ходе их разработки) невозможна. В основном это связано с
1) возможность системы изменять свою конфигурацию в ходе работы (ad-hoc системы c беспроводной связью; системы с частичным обновлением ПО и конфигурации),
2) применением компонентов, для которых нет достаточных для статической верификации спецификации, а есть лишь описание интерфейсов (мульти-вендорные системы, компоненты которых разрабатываются различными компаниями),
3) сложный контекст работы системы (взаимодействие с реальным миром, Интернет).
До недавнего времени при разработке критически важных (safety-critical) систем подобные особенности и компоненты не использовались. Однако сейчас это уже не так, и если в каких-то областях этих проблем нет, то они появятся в ближайшем времени.
Для обеспечения надёжной работы таких систем необходимо использовать динамическую проверку правильности работы системы -- выполнять мониторинг поведения системы в реальном времени, оценивать соответствие наблюдаемого поведения спецификации, вовремя прогнозировать нарушение спецификации и предотвращать их. Существует достаточно много работ, посвящённых runtime monitoring и runtime verification, однако в них остаются открытыми следующие вопросы:
1) работа с разнообразными средствами описания свойств,
2) надёжность применяемых методов анализа и предотвращения сбоев,
3) эффективность алгоритмов анализа.
Этими вопросами и предполагается заняться в данной работе.
1) возможность системы изменять свою конфигурацию в ходе работы (ad-hoc системы c беспроводной связью; системы с частичным обновлением ПО и конфигурации),
2) применением компонентов, для которых нет достаточных для статической верификации спецификации, а есть лишь описание интерфейсов (мульти-вендорные системы, компоненты которых разрабатываются различными компаниями),
3) сложный контекст работы системы (взаимодействие с реальным миром, Интернет).
До недавнего времени при разработке критически важных (safety-critical) систем подобные особенности и компоненты не использовались. Однако сейчас это уже не так, и если в каких-то областях этих проблем нет, то они появятся в ближайшем времени.
Для обеспечения надёжной работы таких систем необходимо использовать динамическую проверку правильности работы системы -- выполнять мониторинг поведения системы в реальном времени, оценивать соответствие наблюдаемого поведения спецификации, вовремя прогнозировать нарушение спецификации и предотвращать их. Существует достаточно много работ, посвящённых runtime monitoring и runtime verification, однако в них остаются открытыми следующие вопросы:
1) работа с разнообразными средствами описания свойств,
2) надёжность применяемых методов анализа и предотвращения сбоев,
3) эффективность алгоритмов анализа.
Этими вопросами и предполагается заняться в данной работе.