Антон Бондарев

В трудовой деятельности является руководителем проектов в департаменте радио-электронных систем компании «Ланит-Терком», где занимается разработкой встроенных и специализированных систем в телекоммуникации, системами управления и системами обработки сигналов. Увлекается системным программированием. Как и любой программист, мечтал написать свою операционную систему, что в итоге и было реализовано в проекте Embox.

---

Применение DSL для выполнения требований стандарта DO-178B

ген. директор ООО “Ембокс” Бондарев Антон Владимирович,
асп. каф. сис. прог. СПбГУ Козлов Антон Павлович

Для программного обеспечения критически важных систем основными стандартами являются не стандарты, описывающие программный интерфейс (API), как, например, POSIX, а документы, регламентирующие процессы разработки, например DO-178B. Следование данному документу подразумевает контроль на всех стадиях жизненного цикла разработки. Для осуществления этого контроля требуется разработать довольно большой пакет документации, в том числе и для набора тестов. Но поскольку по требованиям стандарта жизненный цикл ПО должен иметь V-модель, то есть проходить модификацию на этапах проверки системы, поддержание документации в актуальном состоянии затруднено, так как она разрабатывается на естественном языке. В данном докладе рассматривается метод автоматизации и упрощения процесса разработки ПО, соответствующего стандарту DO-178B, путем применения формализованного специального языка DSL, используемого на всех этапах разработки.

---

• Скачать презентацию в pptx

---

В истории развития методов разработки программного обеспечения стоит выделить несколько этапов:
• Разработка алгоритмов с нуля на машинном языке
• Появление мониторов, позволяющих автоматизировать запуск алгоритмов
• Появление языков высокого уровня
• Появление операционных систем
• Появление кросс-платформенных программных платформ (frameworks).
Причиной, подтолкнувшей индустрию к такому пути развития, являлось желание уменьшить цену и время разработки путем переиспользования ранее разработанных компонент. Для этого потребовалось, чтобы программные интерфейсы этих компонент соответствовали единому стандарту. Для операционных систем таким стандартом стал POSIX — Portable Operating System Interface.

При создании критически важных систем, в отличие от создания обычных, на первый план выходит не скорость и цена разработки, а качество и надёжность полученной системы. Поэтому ПО для подобных систем, должно быть протестировано, верифицировано и сертифицировано до попадания на реальный объект. Всё это отражается на модели разработки, в которую должны быть в обязательном порядке включены перечисленные стадии. Поэтому основным стандартом для подобных систем является не POSIX, описывающий программный интерфейс, а DO-178B (Software Considerations in Airborne Systems and Equipment Certification). И хотя данный документ описывает требования, предъявляемые к процессу разработки ПО для бортовых систем, он может быть использован и для других систем с высокими требованиями по надежности.

DO-178B требует внедрения в процесс наработки критически важного ПО так называемой V-образной модели. В упрощённом виде ее можно представить следующим образом рис 1.:

рис 1. V-образная модель разработки ПО

Данная модель, в отличие от водопадной, предполагает наличие обратной связи между этапами на спадающей и восходящей ветках разработки. Спадающая ветка включает этапы, предшествующие стадии реализации (собственно, написания кода), при этом по временной шкале этапы располагаются с постепенным увеличением детализации требований и архитектуры. На восходящей ветке располагаются этапы, отвечающие за проверку соответствующих требований. На каждом этапе из восходящей ветки в случае несоответствия предъявляемым требованиям процесс может вернуться на уровень, в котором были выявлены нарушения. Причём последним по времени стоит этап проверки на соответствие самым общим требованиям, то есть предъявляемым на начальном этапе работ.

Стандарт DO-178B требует того, чтобы результатом каждого жизненного цикла стали различного рода артефакты, позволяющие провести формальную проверку требований, предъявляемых к данному этапу разработки. Такими артефактами могут являться документы, спецификации, тесты, диаграммы описания архитектуры и непосредственно программный код.

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

При применении формального языка описания требований для системы можно составить модель, которая может быть представлена графом предикатов, и следовательно, может быть проверена на целостность и непротиворечивость.

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

Embox — ОСРВ для встраиваемых систем. Важными особенностями, позволяющими применять данный проект для критически важных систем, являются:
• Статическая сборка целевого образа
• Наличие внутренней модели системы
• Генерация всех необходимых артефактов
• Наличие специализированной системы тестирования
Данный свойства достигаются за счет использования системы сборки, основанной на специально разработанном языке Mybuild. Основной идеей разработки отдельной системы сборки было отделение логики программы, разрабатываемой на обычном языке программирования, от более высокоуровнего описания модулей и системы в целом. Данная мета-информация используется для построения модели системы, которая может быть проверена с помощью формальных методов анализа.

На основе полученной модели генерируется значительное количество артефактов, необходимых для создания системы. Среди них заголовочные файлы с описанием констант и необходимых структур данных, скрипты для линкера, массивы описаний модулей и так далее.

Бизнес-логика отдельных модулей описывается на обычном языке программирования, например языке C. Требования для каждого модуля можно проверить с помощью встроенной системы unit-тестирования. В проекте Embox реализована собственная система unit-тестирования, которая позволяет выполнять тесты отдельных модулей в автоматическом режиме при старте конечного образа.

Окончательная проверка системы на соответствие требованиям осуществляется интегрированным средством тестирования, которое в проекте Embox реализовано на языке TCL. Оно представляет из себя набор файлов с набором тестовых операций для проверки требований, которая осуществляется через подключение к удалённому терминалу.

Таким образом, Embox содержит средства, упрощающие создание систем в соответствии со стандартом DO-178B путем применения специального языка описания модулей (DSL). Данный язык применяется на всех стадиях разработки проекта, и всилу своей формализованности позволяет поддерживать в актуальном состоянии общую модель конечной системы.