Об интеграции формальных методов в задачах верификации операционных систем

Труды Института системного программирования РАН. 2015. Т. 27. № 5. С. 175–190.

Петренко А. К., Кулямин В. В., Хорошилов А. В.

В данной работе ставится задача разработки методов качественной верификации операционных систем, перспективным подходом к решению которой является интеграция различных техник верификации. Результатом успешного решения этой задачи может считаться комбинация методов верификации, которая позволяет проверить всю систему в целом и при этом более тщательно верифицировать наиболее важные ее компоненты и функции, используя для этого более строгие и формальные подходы. На основе опыта ИСП РАН, полученного при выполнении многочисленных проектов по верификации операционных систем с помощью различных методов выявлены артефакты разработки, являющиеся удобными кандидатами на роль точек сопряжения методов статической и динамической верификации ядра операционной системы на основе формальных спецификаций. 
Выделение общих (разделяемых) артефактов предлагается провести на основе рассмотрения типовых задач верификации. Типовые задач, встречающиеся при использовании различных техник верификации, дают основу для интеграции техник и процессов верификации. К таким типовым задачам относятся: определение программного контракта модулей (функций), построение модели окружения, построение пути, демонстрирующего ошибку, увязка уровней абстракции и оценка полноты верификации. В наибольшей степени на роль артефактов представляющих собой точки интеграции претендуют контрактные спецификации, модели окружения и метрики (измерения) полноты верификации.

Ключевые слова: операционная система, тестирование на основе моделей, проверка моделей, дедуктивная верификация, интеграция методов верификации, программные контракты