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


Моделирование окружения драйверов устройств операционной системы Linux.

Захаров И.С., Мутилин В.С., Новиков Е.М., Хорошилов А.В.

Аннотация

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

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

операционная система; драйвер; окружение; верификация

Издание

Труды Института системного программирования РАН, том 25, 2013, стр. 85-112.

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

DOI: 10.15514/ISPRAS-2013-25-6

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