Компиляторы C, Ada и SPARK для архитектуры RISC-V

Компиляторы C, Ada и SPARK для архитектуры RISC-VКомпания AdaCore, производитель средств разработки и верификации ПО критически важных для безопасности встраиваемых систем, внесла свой вклад в поддержку архитектуры RISC-V, выпустив компиляторы для языков C и Ada, а также для языка SPARK – подмножества языка Ada, позволяющего проводить формальную верификацию. Компиляторы AdaCore GNAT Pro сопровождаются документацией для сертификации по стандартам функциональной безопасности DO-178C (авионика), МЭК 61508 (промышленные системы управления), EN 50128 (железнодорожные системы) и ISO 26262 (автоэлектроника). Компиляторы GNAT Pro поддерживают 32-бит и 64-бит RISC-V, а бесплатный вариант компилятора GNAT Community – 32-бит RISC-V.

Процессорная архитектура RISC-V разработана в Университете Беркли и поддерживается консорциумом RISC-V International, объединяющим более 500 компаний, среди которых NVIDIA, NXP, Marvell, Google, Thales, Samsung, Qualcomm и Western Digital. Архитектура RISC-V является открытой и доступна для свободного и бесплатного использования разработчиками в качестве процессорного ядра систем-на-кристалле.

Недавно NVIDIA и AdaCore начали сотрудничество по применению языков программирования Ada и SPARK для разработки критически важного для информационной безопасности (security critical) ПО будущих систем-на-кристалле NVIDIA, построенных на базе открытой архитектуры RISC-V. Переходы NVIDIA на архитектуру RISC-V и на языки Ada и SPARK обусловлены возросшими требованиями к безопасности и защищенности ПО, которые предъявляются новыми ответственными применениями, такими как автоматизированные и автоматические транспортные средства.

На странице www.adacore.com/resources можно загрузить руководство «AdaCore Technologies for Cyber Security» по применению языков Ada и SPARK и продуктов AdaCore для разработки ПО, критически важного для информационной безопасности.

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

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

Добавить комментарий

Ваш адрес email не будет опубликован. Обязательные поля помечены *