Программное обеспечение Vega-C работает на целевом процессоре LEON 2 и будет сертифицировано по стандартам ECSS-E-ST-40C и ECSS-Q-ST-80C (EuropeanCooperationonSpaceStandardization) на уровень критичности для безопасности LevelB. Компания AVIO выбрала язык Ada за то, что благодаря своему синтаксису язык Ada помогает, а часто даже заставляет разработчика создавать код высокого качества, а широкий набор статических (на этапе компиляции) и динамических (на этапе прогона) проверок помогают находить потенциальные уязвимости и угрозы безопасности. Кроме этого, ПО проекта будет эволюционировать в течение многих лет, поэтому хорошая читаемость программ на языке Ada в сочетании с развитой поддержкой модульности и структурируемости, сыграла при выборе языка немаловажную роль.    

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

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

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

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

Дистрибьютор компании AdaCore в России – компания АВД Системы, поставщик средств разработки программного обеспечения критически важных для безопасности сертифицируемых встраиваемых компьютерных систем. Предлагаем предприятиям, заинтересованным в получении дополнительной информации о языках Ada и SPARK и современных технологиях разработки и верификации ПО, проведение бесплатного семинара.