A formal model of a partitioned real-time operating system in Promela

Текущий стандарт надежного программного обеспечения для бортовых контроллеров – это многораздельная операционная система реального времени, которая способна реагировать на события от устройств с ожидаемой скоростью, а также делить процессорное время и память между изолированными разделами. Верификация на основе модели – это метод формальной проверки программного обеспечения, при котором разрабатывается программная модель, а затем она автоматически проверяется на соответствие формальным требованиям. Этот метод позволяет доказать правильность работы модели на всех возможных входных данных, всех возможных способов переключения процессов и взаимодействий. В этой статье описывается формализованная модель открытой многораздельной операционной системы POK, реализованная на языке Promela средства SPIN для формальной верификации методом Model Checking и предназначенная для моделирования поведения: планировщика разделов и процессов; системных вызовов через программное прерывание; библиотеки ядра для работы с примитивами синхронизации и ожиданием процессов; пользовательский код, осуществляющий работу нескольких процессов в разных разделах, которые синхронизируются через семафоры. Данный подход может быть использован для проверки корректности синхронизации, работы алгоритмов планировщика, корректного доступа к данным из разных разделов путем задания соответствующих требований в виде формул темпоральной логики линейного времени.