RUS  ENG
Полная версия
ЖУРНАЛЫ // Моделирование и анализ информационных систем // Архив

Модел. и анализ информ. систем, 2024, том 31, номер 4, страницы 474–494 (Mi mais836)

Эта публикация цитируется в 1 статье

Theory of computing

Точный тест планируемости для систем реального времени с абстрактным планировщиком на мультипроцессорных платформах

Н. О. Гаранина

Институт автоматики и электрометрии СО РАН, Новосибирск, Россия

Аннотация: Эта статья посвящена использованию метода верификации моделей для точного теста планируемости систем реального времени, выполняющихся на мультипроцессорных платформах. Чтобы использовать этот метод, мы формально описываем системы реального времени с абстрактным планировщиком, используя модели Крипке. Эта формализация содержит термины, достаточные для специализации абстрактного планировщика. Мы иллюстрируем наш подход, явно определяя планировщики, которые учитывают вытеснение/невытеснение задач и глобальный фиксированный приоритет или приоритет ближайшего дедлайна в различных сочетаниях. Свойство безопасности (планируемости) систем реального времени сформулировано с помощью линейной темпоральной логики LTL. Формализация систем реального времени как моделей Крипке и задание свойства безопасности (планируемости) как формулы LTL позволяет свести точный тест планируемости таких систем к задаче верификации моделей. Мы апробируем этот подход к точному тесту планируемости, реализуя на Promela — входном языке инструмента верификации моделей SPIN — нашу формализацию систем реального времени с невытесняющим планировщиком с глобальным фиксированным приоритетом (NP-GFP), вытесняющим планировщиком с глобальным фиксированным приоритетом (P-GFP), невытесняющим планировщиком с приоритетом ближайшего дедлайна (NP-EDF) и вытесняющим планировщиком с приоритетом ближайшего дедлайна (P-EDF). Мы проводим эксперименты в SPIN для доказательства/опровержения свойства безопасности (планируемости), чтобы оценить эффективность нашего подхода. Мы предлагаем эвристическую оценку планируемости системы реального времени на основе доказуемости небезопасности и недоказуемости безопасности системы реального времени при выполнении на мультипроцессорных платформах с числом процессоров, отличающимся на единицу.

Ключевые слова: системы реального времени, точный тест на планируемость, модели Крипке, проверка моделей, Promela, SPIN.

УДК: 004.415.52

MSC: 93-04

Поступила в редакцию: 06.11.2024
Исправленный вариант: 15.11.2024
Принята в печать: 30.11.2024

DOI: 10.18255/1818-1015-2024-4-474-494



© МИАН, 2025