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


Верификация и анализ вариабельных операционных систем

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

Аннотация

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

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

операционная система, семейство систем, модель вариабельности, верификация, статический анализ, проверка моделей, проверка типов, покрытие кода, покрывающий набор, итеративное уточнение модели на основе контрпримеров

Издание

Труды Института системного программирования РАН, том 28, вып. 3, 2016, стр. 189-208.

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

DOI: 10.15514/ISPRAS-2016-28(3)-12

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