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

6 WWW.SOEL.RU На правах рекламы РЫНОК СОВРЕМЕННАЯ ЭЛЕКТРОНИКА ◆ № 5 2019 NVIDIA ПЕРЕХОДИТ НА ЯЗЫК A DA Компания AdaCore, производитель средств разработки и верификации ПО кри- тических для безопасности встраиваемых систем, объявила о начале сотрудничества с корпорацией NVIDIA по применению язы- ков программирования Ada и SPARK при разработке критического для информаци- онной безопасности (security critical) ПО бу- дущих систем-на-кристалле NVIDIA, постро- енных на базе новой открытой архитекту- ры RISC-V. Переходы NVIDIA на архитектуру RISC-V и на языки Ada и SPARK обусловлены воз- росшими требованиями к безопасности и защищённости ПО, предъявляемыми новы- ми ответственными применениями, таки- ми как автоматизированные и автоматиче- ские транспортные средства. На странице www.adacore.com/resources можно загру- зить руководство «AdaCore Technologies for Cyber Security» по применению языков Ada и SPARK и продуктов AdaCore для раз- работки ПО, критически важного для ин- формационной безопасности. Архитектура RISC-V разработана в Уни- верситете Беркли и поддерживается кон- сорциумом RISC-V Foundation, объединяю- щим более 200 компаний, таких как NVIDIA, NXP, Marvell, Google, Thales, Samsung, Qualcomm и Western Digital. Недавно ком- пания AdaCore стала членом консорциума RISC-V Foundation, и внесла свой вклад в поддержку архитектуры выпуском компи- ляторов GNAT Pro Ada и GNAT Pro C для 32-бит и 64-бит RISC-V, а также бесплатно- го варианта компилятора GNAT Community для 32-бит RISC-V. Язык программирования Ada создавался специально для разработки ПО с повышен- ными требованиями к надёжности. В насто- ящее время Ada является основным языком для разработки ПО систем, критически важ- ных для безопасности. Язык Ada является международным стандартом ISO 8652. В последней редак- ции стандарта ISO 8652-2012 (Ada 2012) введена конструкция для задания «кон- трактов» – требований к результатам ра- боты программного модуля, описанных непосредственно в тексте программы на языке Ada. «Контракт» предназначен для использования компилятором для встав- ки динамических проверок или средства- ми статического анализа для формальной верификации. Язык SPARK является подмножеством Ada 2012, позволяющим проводить фор- мальную верификацию ПО – доказатель- ство математическими методами, что ПО делает то, что от него требуется и не де- лает того, что не требуется. Недавно компания AdaCore завершила исследовательский проект, целью кото- рого было продемонстрировать примене- ние формальных методов для выполне- ния требований стандарта функциональ- ной безопасности автомобильного ПО ISO 26262 в части обеспечения «Freedom from Interference» (Свободы от Вторже- ний) – защиты приложений с высоким уровнем критичности для безопасности ASIL (Automotive Safety Integrity Level) от влияния сбоев, возникших в приложени- ях с низким уровнем критичности ASIL, унаследованных (legacy) из предыду- щих проектов и написанных на языке Си. В этом проекте компания AdaCore вы- ступила не только поставщиком средств формальной верификации ПО на языке SPARK, но и разработчиком методологии создания «контрактов» для обеспечения требований Freedom from Interference в ISO 26262, а также технологии «гибрид- ной верификации» – совмещения фор- мальных методов с традиционной вери- фикацией ПО, основанной на тестиро- вании. Комплекс инструментальных средств 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 (космическая техника). Другие продукты AdaCore: ● CodePeer – статический анализатор / де- тектор потенциальных ошибок и уязвимо- стей в программах на языке Ada; ● SPARK Pro – комплекс средств верифи- кации ПО на языке SPARK – формаль- но верифицируемом подмножестве язы- ка Ada; ● QGen – квалифицируемый генератор программного кода на языках MISRA C и SPARK из моделей Simulink/Stateflow. Дистрибьютор компании AdaCore в Рос- сии – компания АВД Системы, поставщик средств разработки программного обеспе- чения критически важных для безопасности сертифицируемых встраиваемых компью- терных систем. Предлагаем предприятиям, заинтересованным в получении дополни- тельной информации о языках Ada и SPARK и современных технологиях разработки и верификации ПО, проведение бесплатно- го семинара. www.avdsys.ru/ada