Развитие метода контрактных спецификаций для верификации модулей ядра операционной системы Linux.

Авторы

Е.М. Новиков.

Аннотация

Диссертация посвящена развитию метода контрактных спецификаций для верификации модулей ядра Linux. Актуальность темы обусловлена тем, что на сегодняшний день не существует методов контрактных спецификаций, учитывающих особенности процесса разработки ядра Linux и позволяющих проверять выполнение правил корректного использования программного интерфейса ядра в модулях посредством различных инструментов верификации. Научной новизной обладают следующие результаты работы: новый метод описания в виде контрактных спецификаций правил корректного использования программного интерфейса ядра Linux; новое аспектно-ориентированное расширение языка программирования Си с поддержкой расширений компилятора GCC; новый метод автоматизированного инструментирования исходного кода модулей ядра Linux, который позволяет в дальнейшем применять различные инструменты верификации для проверки выполнения правил, заданных контрактными спецификациями; новый метод автоматизированной поддержки корректности и согласованности контрактных спецификаций в условиях изменения программного интерфейса ядра Linux. На основе предлагаемого в работе метода контрактных спецификаций были разработаны и использованы на практике спецификации для 34 правил корректного использования программного интерфейса ядра Linux. Инструментарий, реализующий предлагаемый метод контрактных спецификаций, был включен в состав конфигурируемой системы статической верификации модулей ядра ОС Linux. По результатам верификации модулей нескольких версий ядра Linux было выявлено более 125 ошибок, признанных разработчиками ядра.

Полный текст статьи в формате pdf

Издание

Диссертация на соискание ученой степени к.ф.-м.н., Москва, 2013 г.

Научная группа

Технологии программирования

Все публикации за 2013 год

Все публикации