Сборники трудов ИСП РАН


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

А.К.Петренко (ИСП РАН, Москва; МГУ, Москва; МФТИ, Москва; ВШЭ, Москва), В.В.Кулямин (ИСП РАН, Москва; МГУ, Москва; ВШЭ, Москва), А.В.Хорошилов (ИСП РАН, Москва; МГУ, Москва; МФТИ, Москва; ВШЭ, Москва)

Аннотация

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

Ключевые слова

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

Издание

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

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2015-27(5)-10

Полный текст статьи в формате pdf Вернуться к содержанию тома