Современная электроника №2/2019

РЫНОК 9 WWW.SOEL.RU СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 2 2019 На правах рекламы СОВРЕМЕННЫЕ ТЕХНОЛОГИИ П РОГРАММНОЕ ОБЕСПЕЧЕНИЕ РАКЕТЫ - НОСИТЕЛЯ V EGA -C РАЗРАБАТЫВАЕТСЯ НА ЯЗЫКЕ A DA Ракета-носитель 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 (Euro- pean 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. Дистрибьютор компании AdaCore в Рос- сии – компания «АВД Системы» – постав- щик средств разработки программного обе- спечения критически важных для безопас- ности сертифицируемых встраиваемых компьютерных систем. Предприятиям, заинтересованным в полу- чении дополнительной информации о язы- ках Ada и SPARK и современных технологи- ях разработки и верификации ПО, предла- гается проведение бесплатного семинара. www.avdsys.ru/ada