Аннотация:
Методы и инструменты автоматической статической верификации позволяют выявить все ошибки искомых видов в целевых программах при выполнении определенных предположений даже в условиях отсутствия полных моделей и формальных спецификаций. Эта возможность является основой предлагаемого в работе метода инкрементального построения спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем. Данный метод был реализован в системе статической верификации Klever и применен для проверки подсистемы поддержки терминальных устройств ядра ОС Linux.
Ключевые слова:операционная система, монолитное ядро, качество программной системы, статическая верификация, формальная спецификация, декомпозиция программной системы, модель окружения.
Полный текст:
PDF файл (618 kB)