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


Инкрементальное построение спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем

Захаров И.С. (ИСП РАН, Москва, Россия)
Новиков Е.М. (ИСП РАН, Москва, Россия)

Аннотация

Методы и инструменты автоматической статической верификации позволяют выявить все ошибки искомых видов в целевых программах при выполнении определенных предположений даже в условиях отсутствия полных моделей и формальных спецификаций. Эта возможность является основой предлагаемого в работе метода инкрементального построения спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем. Данный метод был реализован в системе статической верификации Klever и применен для проверки подсистемы поддержки терминальных устройств ядра ОС Linux.

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

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

Издание

Труды Института системного программирования РАН, том 29, вып. 6, 2017, стр. 25-48.

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

DOI: 10.15514/ISPRAS-2017-29(6)-2

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