Аннотация:
В работе рассматривается задача проверки допустимости конфигураций модульных вычислительных систем реального времени (МВС РВ). Конфигурация считается допустимой, если все работы успевают выполниться в рамках своих директивных сроков. В статье приведены формальные определения конфигурации МВС РВ и временной диаграммы (ВД) ее функционирования. ВД, соответствующая заданной конфигурации, необходима для проверки критерия допустимости для данной конфигурации. Автором предложена обобщенная модель функционирования таких систем, основанная на математическом аппарате временных автоматов с остановкой таймеров. Представлен метод построения модели конкретной МВС РВ по описанию ее конфигурации. Модель позволяет получить временную диаграмму функционирования системы по вычислению соответствующей сети автоматов. Математический аппарат сетей временных автоматов позволил доказать, что модель детерминирована, а также удовлетворяет ряду требований корректности, выделенных из спецификаций на МВС РВ. Предложенные методы реализованы программно. Проведено экспериментальное сравнение предложенного подхода с альтернативным подходом (верификацией моделей систем), использующим такой же математический аппарат. Эксперименты подтвердили эффективность разработанной модели. Для апробации на данных, приближенных к реальным, программная реализация модели была также интегрирована c существующим средством планирования вычислений в МВС РВ, используемым в промышленности. Результаты апробации подтвердили применимость предложенного подхода на практике.
Ключевые слова:модульные вычислительные системы, проверка корректности расписаний, временные автоматы, системы реального времени.