Программное обеспечение ракеты-носителя Vega-C разрабатывается на языке Ada

Ракета-носитель Vega легкого класса (1500 кг полезной нагрузки) Европейского космического агентства предназначена для выведения на орбиту малых спутников и за время коммерческой эксплуатации с 2012 года уже совершила 13 успешных запусков. Итальянская компания AVIO разрабатывает новый вариант носителя Vega-C (Consolidation), у которого полезная нагрузка будет увеличена до 2200 кг и будет снижена стоимость выведения. Квалификационный запуск Vega-C планируется на середину 2019 года.

Для разработки программного обеспечения систем управления полетом, ориентирования и навигации компания AVIO выбрала язык программирования Ada и комплекс инструментальных средств GNAT Pro Assurance Ada компании AdaСore. ПО Vega-C работает на целевом процессоре LEON 2 и будет сертифицировано по стандартам ECSS-E-ST-40C и ECSS-Q-ST-80C (European Cooperation on Space Standardization) на уровень критичности для безопасности Level B. Компания AVIO выбрала Ada, поскольку благодаря своему синтаксису данный язык помогает, а часто и заставляет разработчика создавать код высокого качества, а широкий набор статических (на этапе компиляции) и динамических (на этапе прогона) проверок помогают находить потенциальные уязвимости и угрозы безопасности. Кроме этого, ПО проекта будет эволюционировать в течение многих лет, поэтому хорошая читаемость программ на языке Ada вкупе с развитой поддержкой модульности и структурируемости сыграла при выборе языка немаловажную роль.

Язык программирования Ada создавался специально для разработки ПО с повышенными требованиями к надежности, и в настоящее время Ada является основным языком для разработки ПО систем, критически важных для безопасности и сертифицируемых по стандартам функциональной (safety) и информационной (security) безопасности. Язык Ada — это международный стандарт ISO 8652. В последней редакции стандарта ISO 8652-2012 (Ada 2012) введена конструкция для задания «контрактов» — требований к результатам работы программного модуля, описанных непосредственно в тексте программы на языке Ada. «Контракт» предназначен для использования компилятором для вставки динамических проверок или средствами статического анализа для формальной верификации — доказательства математическими методами, что ПО делает только все необходимое и не делает того, что не требуется.

Комплекс инструментальных средств GNAT Pro Ada включает компилятор, поддерживающий все версии стандартов Ada (Ada 83, Ada 95, Ada 2005 и Ada 2012), интегрированную среду разработки, визуальный отладчик, средства автоматизации тестирования, средства статического анализа (контроль стандартов кодирования, сбор метрик программного кода, анализатор стека), средства формальной верификации (доказательства корректности работы ПО с помощью математических методов) и средства интеграции Ada и C/C++ программ. Комплекс GNAT Pro Ada поддерживает микропроцессорные архитектуры x86, PowerPC, ARM и LEON. Поддерживаются целевые платформы с операционными системами LynxOS, PikeOS, QNX, VxWorks, Embedded Linux и без ОС (bare metal). Вариант GNAT Pro Assurance предназначен для разработки ПО систем, сертифицируемых по стандартам функциональной безопасности, таких как DO-178C (авионика), EN 50128 (ж/д системы), ISO 26262 (автоэлектроника) и ECSS-E-ST-40C/Q-ST-80C (космическая техника).

Для тестирования ПО Vega-C компания AVIO применяет GNATemulator — эмулятор целевой (target) платформы на инструментальной машине. Это позволяет проводить тестирование ПО при отсутствии реального аппаратного прототипа целевой платформы и избежать двух различных конфигураций компилятора при проведении тестирования одной части ПО в native-режиме на инструментальной машине, а другой части ПО в cross-режиме на целевой платформе.

Другие продукты AdaCore: CodePeer — статический анализатор/детектор потенциальных ошибок и уязвимостей в программах на языке Ada, SPARK Pro — комплекс средств верификации ПО на языке SPARK, формально верифицируемом подмножестве языка Ada, QGen — квалифицируемый генератор программного кода на языках MISRA C и SPARK из моделей Simulink/Stateflow.

www.avdsys.ru/ada