JTEKT выбрала язык SPARK для верификации ПО электроусилителей рулевого управления

Японская корпорация JTEKT, производитель систем усиления рулевого управления, выбрала язык программирования SPARK и инструментальные средства компании AdaCore для разработки и верификации критического для безопасности ПО, сертифицируемого по стандарту ISO 26262. В автономных транспортных средствах система рулевого управления должна взаимодействовать с другими системами, например с системой контроля полосы движения, и ее программное обеспечение имеет наивысший уровень критичности для безопасности – ASIL D (Automotive Safety Integrity Level) стандарта ISO 26262.

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

Для разработки и верификации ПО электроусилителей руля JTEKT применяет комплекс средств верификации SPARK Pro, а также GNAT Pro CCG (Common Code Generator) – транслятор программы на языке Ada/SPARK в программу на языке C. Применение CCG позволяет использовать всю имеющуюся в компании инфраструктуру разработки на языке С. Недавно SPARK Pro и GNAT Pro CCG были квалифицированы по стандартам МЭК 61508 и ISO 26262, которые определяют четыре уровня критичности для безопасности SIL (Safety Integrity Level) и три категории инструментальных средств для обеспечения заданного уровня SIL. Транслятор GNAT Pro CCG квалифицирован по наивысшим категориям T3 стандарта МЭК 61508 и TCL3 (Tool Confidence Level) стандарта ISO 26262, а комплекс SPARК Pro – по категориям T2 МЭК 61508 и TCL3 ISO 26262.

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

• GNAT Pro – компилятор и комплекс средств разработки на языке Ada, поддерживает все редакции языка Ada83, Ada95, Ada2005 и Ada2012;
• CodePeer – статический анализатор / детектор потенциальных ошибок и уязвимостей в программах на языке Ada;
• SPARK Pro – комплекс средств верификации ПО на языке SPARK, формально верифицируемом подмножестве языка Ada;
• QGen – квалифицируемый генератор программного кода на языках MISRA C и SPARK из моделей Simulink/Stateflow.

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