Мониторинг и тестирование на основе многоуровневых спецификаций программ

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