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


Построение спецификаций программных интерфейсов в открытой системе покомпонентной верификации ядра Linux.

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

Аннотация

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

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

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

Издание

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

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

DOI: 10.15514/ISPRAS-2013-24-13

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