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


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

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

Аннотация

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

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

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

Издание

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

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

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

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