Формальная верификация компонентов ядра для операционных систем с открытым исходным кодом

Аннотация Задача обеспечения стабильности и надежности системного программного обеспечения с использованием средств статического анализа кода и формальной верификации является актуальной и важной в современном мире. В данной работе подробно разобраны методология и функционал моделирования и анализа формального метода Event-b на примере системы контроля машин на мосту. Детально, с объемными теоритическими вставками, разобрана исходная модель системы контроля машин на мосту, с подробными описаниями аксиом, инвариантов, событий, вводимых понятий и ее пошаговой формальной верификации. В результате чего видно, что требования начальной модели были наивными, и также видно, как меняется модель системы после ее формальной верификации. Из чего следует вывод, что формальное доказательство модели помогает нахождению в ней несоответствий. Методология и функционал Event-b разбирались на примерах из Event-b book. Так же, на примере этой модели разобран функционал и инструментарий среды разработки для Event-B – The Rodin Platform. Подробно и пошагово построены и верифицированы модели систем из обучающей книги Rodin User`s Handbook. С использованием The Rodin Platform сформулированы и формально доказаны инварианты некоторых других систем. Пошагово разобран пример доказательства арифметических тождеств с использованием метода математической индукции и без него. Относительно решена проблема реализации математической индукции в The Rodin Platform. Разобрана теоритическая информация о ядре, методах и алгоритмах верификации драйверов операционной системы Linux.