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


Архитектура Linux Driver Verification.

В.С. Мутилин, Е.М. Новиков, А.В. Страх, А.В. Хорошилов, П.Е. Швед.

Аннотация

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

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

статический анализ кода; правила корректности; верификация драйверов устройств; моделирование окружения драйвера; аспектно-ориентированное программирование; верификатор достижимости; визуализация трассы ошибки

Издание

Труды Института системного программирования РАН, том 20, 2011, стр. 163-187.

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

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