Модель партицированной операционной системы для целей формальной верификации (Partitioned OS model for formal verification purposes)

Программа представляет собой формализованную модель партицированной операционной системы, реализованной на языке Promela средства SPIN для формальной верификации методом Model Checking и предназначена для моделирования поведения: планировщика партиций и процессов методом round-robin; системных вызовов (syscalls) через программное прерывание; библиотеки ядра для работы с примитивами синхронизации и ожиданием процессов; пользовательского кода, осуществляющего работу нескольких процессов в разных партициях, синхронизирующихся через примитив семафор. Программа может быть использована для проверки корректности синхронизации, работы планировщика, корректного доступа к данным из разных партиций, путем задания соответствующих требований в виде формул темпоральной логики линейного времени. Тип ЭВМ: IBM PC-совмест. ПК; ОС: Linux.