Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы

В связи с высокой сложностью современных операционных систем (ОС) для спецификации даже отдельных аспектов их функциональности, как, например, функций безопасности, приходится использовать достаточно сложные модели на высокоуровневых языках. При этом задача верификации соответствия таким моделям серьезно усложняется из-за необходимости установления связей между реализацией операционной системы и моделью, представленными на сильно отличающихся языках. В данной работе мы представляем методику установления и поддержания таких связей, которую можно эффективно использовать при тестировании и мониторинге операционных систем. Описанная методика была успешно применена при тестировании и мониторинге компонентов ядра операционной системы Linux с использованием моделей на Event-B.