Компиляторы Ada и C компании AdaCore квалифицированы по МЭК 61508 и ИСО 26262

Компания AdaCore, производитель средств разработки и верификации ПО критически важных для безопасности встраиваемых систем, провела квалификацию своих компиляторов и других инструментальных средств по стандартам функциональной безопасности МЭК 61508 (промышленные системы управления) и ИСО 26262 (автомобильная электроника). Квалификация проведена для компиляторов GNAT Pro Ada и GNAT Pro C, комплекса SPARK Pro средств верификации ПО на языке SPARK – формально верифицируемом подмножестве языка Ada, а также для нового продукта CCG (Common Code Generator) – транслятора программы на языке Ada/SPARK в программу на языке C. Транслятор CCG предназначен для генерации кода для процессоров, не поддерживаемых компилятором Ada, но имеющих компилятор C.

Стандарты МЭК 61508 «Функциональная безопасность электрических / электронных / программируемых электронных систем» и ИСО 26262 «Дорожные транспортные средства – функциональная безопасность» определяют четыре уровня критичности для безопасности, SIL (Safety Integrity Level), и три категории инструментальных средств для обеспечения заданного уровня. Компиляторы GNAT Pro и CCG квалифицированы по наивысшей категории T3 стандарта МЭК 61508 и TCL3 (Tool Confidence Level) стандарта ИСО 26262, а комплекс SPARК Pro – по категории T2 МЭК 61508 и TCL3 ИСО 26262.

Компиляторы GNAT Pro Ada и GNAT Pro C поддерживают процессорные архитектуры x86, PowerPC, ARM, LEON, RISC-V и целевые платформы с операционными системами LynxOS, PikeOS, VxWorks, QNX, Embedded Linux, а также без операционной системы (bare metal).

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

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

www.avdsys.ru/ada