Модель партицированной операционной системы для целей формальной верификации (Partitioned OS model for formal verification purposes)
Partitioned OS model for formal verification purposes Модель партицированной операционной системы для целей формальной верификации
Программа представляет собой формализованную модель партицированной операционной системы, реализованной на языке Promela средства SPIN для формальной верификации методом Model Checking и предназначена для моделирования поведения: планировщика партиций и процессов методом round-robin; системных вызовов (syscalls) через программное прерывание; библиотеки ядра для работы с примитивами синхронизации и ожиданием процессов; пользовательского кода, осуществляющего работу нескольких процессов в разных партициях, синхронизирующихся через примитив семафор. Программа может быть использована для проверки корректности синхронизации, работы планировщика, корректного доступа к данным из разных партиций, путем задания соответствующих требований в виде формул темпоральной логики линейного времени. Тип ЭВМ: IBM PC-совмест. ПК; ОС: Linux.
Моделирование поведения: планировщика партиций и процессов методом round-robin; системных вызовов (syscalls) через программное прерывание; библиотеки ядра для работы с примитивами синхронизации и ожиданием процессов; пользовательского кода, осуществляющего работу нескольких процессов в разных партициях, синхронизирующихся через примитив семафор.
Сергей
Старолетов
Михайлович
Доцент
Кандидат физико-математических наук
Доцент
-
-
-
РОССИЯ
Андрей
Марков
Михайлович
Ректор
РОССИЯ
20.53.19
Средства обработки и поиска информации
01.02.EW
COMPUTER SCIENCE, SOFTWARE ENGINEERING
Сергей
Старолетов
Михайлович
100%
РОССИЯ
АлтГТУ
Федеральное государственное бюджетное образовательное учреждение высшего образования "Алтайский государственный технический университет им. И.И. Ползунова"
1022201517854
Организация
Министерство науки и высшего образования Российской Федерации
Федеральные государственные бюджетные учреждения