Проблема неопределенности в анализе трасс на основе высокоуровневых моделей в контексте динамической верификации

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