AdaCore（エイダコア）は6月24日、ジェイテクト（JTEKT）、自動車用電動パワーステアリング・システムの製造メーカが、安全が重視されるパワーステアリング・システム・ソフトウェアの開発を支援するために、AdaCoreのSPARK ProツールスイートとGNAT Pro Common Code Generator（CCG）を採用したことを発表した。
AdaCoreのメンターシップ・プログラムを利用することにより、SPARKテクノロジーを短期間で導入することが可能となり、JTEKTは、SPARK 言語（Ada言語サブセット）と形式手法を応用して、システムのCコードの単体テストと検証が容易となり、その正しさを証明する方法を実証した。SPARKコードをCソースコードに変換するCCGを使用することにより、SPARKの長所を活用しながら、JTEKTは開発済のCコードベースの設計資産の重要な安全特性を証明できるようになった。
パワーステアリング・システムの制御ソフトウェアは、レーンキープアシストなどの自動運転システムと安全に通信する必要がある。誤作動により、生命を脅かしたり致命的な傷害が発生したりする可能性があるため、同システムは、ISO 26262標準で定義されたハザードの最も厳格な自動車用安全度水準（ASIL）Dに分類される。
■ISO 26262 ならびに ASIL Dについて
ISO 26262は、自動車システムの機能安全規格であり、電気/電子/プログラマブル電子（ "E / E / PE"）システムの一般的なIEC 61508規格の分野規格。自動車の安全ライフサイクルのフェーズとそれに関連するアクティビティを定義し、リスクベースのアプローチを使用して、自動車用安全度水準（ASIL）と関連する要件を規定する。システムの機能分析は、機能不全が発生した場合の潜在的な危険と、生命ならびに資産への影響に焦点を当てている。ASILは、A（最低）からD（最高）で定義され、故障が曝露される確率、ドライバがハザードを回避できるか否か、ならびにハザードの発生の重大度が考慮されている。ASIL Dは、機能不全によって、生命に関わる、または致命的な傷害が発生する可能性を示す。そのため、安全性への目標が十分に達成されているかの保証が重要だ。
SPARK Proは、Ada言語サブセット対応のツールセットで、開発エンジニアは数学に基づいた厳格さで特定の脆弱性（バッファオーバーフロー、ゼロ除算、非初期化変数の参照等）がないことなど、ソースコードのプロパティを形式検証し、任意の表明（Assertion）を証明することができる。CCGを使用すると、Adaコンパイラが対応していないターゲットも含めて、SPARKアプリケーションをCコードにクロスコンパイルすることができる。SPARK ProとCCGはISO 26262およびIEC61508の機能安全規格への適合が認定されている。
「私たちは数年前から、信頼性への要求が高まる自動車ソフトウェアに対して、理論的に裏付けされた形式手法を研究している中で、SPARKを知ることができ喜ばしく思っております」と、JTEKTの先行システム開発部上席主担当、米木真哉氏は語っている。「AdaCoreのツールは、セーフティ・クリティカルなソフトウェアテストの開発コストを低減し、安全かつ堅牢な量産コード開発に有効であると確信しています」
「SPARKの形式手法を使用してCコードの正しさを証明することは、自動車の安全/セキュリティに関する最先端技術です」と、AdaCoreの日本営業責任者であるジュアン・カルロス・ベルネド氏（Juan Carlos Bernedo）は語っている。「開発エンジニアにとって、自動車業界の最高レベルの保証基準を満足するソフトウェアを開発する上で、SPARKは費用対効果の高いソリューションの選択肢になりつつあります。JTEKTの事例は、Cコンパイラを提供するソフトウェア・プロバイダーが、SPARK言語とツールセットの導入、活用方法を示しています」
