Аннотация:
Современные операционные системы реального времени являются сложным продуктом, разрабатываемым многими поставщиками: непосредственными разработчиками ОС, поставщиками пакета поддержки аппаратуры, разработчиками драйверов устройств и т.д. Такие ОС спроектированы так, чтобы иметь возможность запускаться на различном оборудовании, часто имеющем ограниченные ресурсы. Встраиваемые ОС содержат множество настроек и драйверов для поддержки разной аппаратуры. Большинство из этих драйверов являются излишними для запуска ОС на каком-то конкретном оборудовании. ОС статически конфигурируется для выбора набора драйверов и настроек для каждого типа аппаратуры. Модульность ОС упрощает как разработку ОС, так и ее конфигурирование. Разделение ОС на изолированные модули с фиксированными интерфейсами уменьшает необходимость взаимодействия между разработчиками в ходе совместной разработки. Мы используем формальные модели для описания компонентов и их взаимодействия. Использование формальных моделей приносит большую пользу. Описываемые модели содержат достаточно информации для генерации исходного кода компонента на языке Си. Предоставляемые модели являются исполняемыми, что позволяет человеку, отвечающему за конфигурацию, быстро проверить правильность заданной конфигурации. Кроме того, модель содержит ограничения на конфигурационные параметры. Примером таких ограничений являются ограничения на внутреннюю согласованность модели. При генерации исходного кода такие ограничения транслируются в специальные проверки на уровне исходного кода. Следовательно, ограничениями могут быть проверены как во время симуляции модели, так и во время исполнения исходного кода. В данной работе представлен подход к описанию таких моделей на языке программирования Scala. Мы успешно апробировали данный подход на основе ОС реального времени JetOS.