Способ проверки корректности планировщика задач операционной системы реального времени с помощью сетей Петри

В статье предложен способ проверки корректности функционирования планировщика задач операционной системы реального времени с применением модели на базе временной сети Петри. Проведен обзор различных политик планировщиков задач операционной системы реального времени. Приведен анализ применения моделей временных сетей Петри для проверки планирования задач операционной системы реального времени на ранней стадии процесса проектирования бортовой аппаратуры космического аппарата с целью определения требуемых вычислительных ресурсов при использовании различных аппаратных конфигураций. Целью исследования является разработка способа проверки корректности функционирования планировщика задач операционной системы реального времени при различных аппаратных конфигурациях вычислительных систем бортового оборудования. По результатам исследований установлено, что технические параметры вычислительной системы бортовой аппаратуры космических аппаратов влияют на стабильность функционирования планировщика операционной системы реального времени. Большое значение для малых космических аппаратов имеют технические ограничения вычислительных платформ, построенных на базе микроконтроллеров. Дальнейшее эволюционное развитие проектируемой системы возможно за счет расширения моделей для различных вычислительных систем, что обеспечит соответствие свойств планировщика задач операционной системы реального времени заданным аппаратным ограничениям.