AdaCore выпустила комплекc средств разработки и верификации ПО на языке Ada для QNX

Софт
мобильная версия
, Текст: Дмитрий Степанов

AdaCore, производитель компилятора и средств разработки ПО для языка программирования Ada, анонсировал поддержку инструментального комплекса GNAT Pro для встраиваемой операционной системы реального времени QNX – одной из самых распространенных в мире и в России ОСРВ для ответственных встраиваемых применений.

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

Комплекс инструментальных средств GNAT Pro включает в себя компилятор, поддерживающий все версии стандартов Ada (Ada 83, Ada 95, Ada 2005 и Ada 2012), интегрированную среду разработки, визуальный отладчик, средства автоматизации тестирования, средства статического анализа (контроль стандартов кодирования, сбор метрик программного кода, анализатор стека), средства формальной верификации (доказательства корректности работы ПО с помощью математических методов) и средства интеграции Ada и C/C++ программ. 

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

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