デンソー：長崎県立大学との研究プロジェクトでAdaCore社SPARKを採用
AdaCore（エイダコア）は15日、デンソー向け研究プロジェクト「Freedom from Interference（以下FFI）を実証するためフォーマルメソッドの適用」が成功裏に終了したと発表した。
このプロジェクトはデンソーと長崎県立大学との共同研究。そのゴールは安全性が決定的に重要な（クリティカルな）自動車用アプリケーションを、自動車の電気/電子機能安全についての国際規格「ISO 26262 Road vehicles - Functional safety」に沿って開発を簡素化すること。レガシーなC言語コードが多くを占める自動車システムにおいて、設計方法「VDM（Vienna Development Method）」と実装言語「SPARK」を有効に使用できるかを調査した。
SPARKのソフトウェアコンポーネントは、ISO 26262（FFI）の要求に従って、発生しうるレガシーCコードの妨害から保護されなければならない。デンソーは、SPARK Proテクノロジで証明されたAdaCoreのフォーマルメソッドに関する専門的な知識と経験を評価し、AdaCoreをパートナーとして選んだ。
1994年に設立されたAdaCoreは、ミッション・クリティカル、セーフティ・クリティカル、かつセキュリティ・クリティカルなシステムのためにソフトウェア開発・検証ツールを提供している。「GNAT Pro Ada」「CodePeer」「SPARK Pro」「QGen」の4つが主力商品だ。
プロジェクトのフェーズ1ではAdaCoreと長崎県立大学はFFIの問題点についての調査を行った。長崎県立大学のチームはフォーマルメソッドの使用について分析し、SPARKのアプローチによってシステムの安全性の検証作業を大幅に簡素化できると判断した。
AdaCoreは、SPARK技術によって高いASIL（Automotive Safety Integrity Level）を持つ（クリティカルな）コンポーネントそれ自体にエラーがないことを証明し、検証作業を簡略化する。またAdaCoreはASILが低いCコードに、SPARKの実行可能なコントラクト（事前条件と事後条件）を追加するガイドラインを作成した。このコントラクトで、クリティカルではないコンポーネントの障害からクリティカルなコンポーネントを保護し、安全性を証明するのに役立つ。
フェーズ1の終了後、デンソーはAdaCoreと長崎県立大学がフェーズ2に進むことに合意した。フェーズ2でAdaCoreはソフトウェアアーキテクチャの安全解析のより一般的な問題に対してもフォーマルメソッドを適用可能か探った。長崎県立大学では、VDMを使用して、障害の連鎖を検出/防止するための安全対策と安全機構を適用するための指針を策定。フェーズ2は2017年10月に完了した。
「AdaCoreのSPARK技術は、フォーマルメソッドをクリティカルな自動車用ソフトウェアのための実用的なツールにします。デンソーのFFIプロジェクトで、その利点を実際に示す機会を与えていただいたことを嬉しく思っています」とAdaCoreの自動車市場製品担当マネージャー、ジュアン・カルロス・ベルネドは語っている。
「よくある質問は、C言語のレガシーコードが多い既存システムにフォーマルメソッドが応用できるかについてです。我々のデンソーとの研究で、従来のテスト中心の検証手法に、SPARKを容易に統合でき、結果としてソフトウェアの信頼性、安全性、セキュリティに対して高いレベルの信頼性を獲得できます」
「AdaCore 社はツールベンダーであるだけではなく、優れた研究パートナーでもあります」とデンソー東京支社電子基盤先行開発室の東道担当課長は語っている。「このプロジェクトでは、デンソーから提示した研究課題や発想を素早く理解して、実りある議論を進めることができました。特にフェーズ2に向けての提案では、有力なオープンソースを活用するアイディアを提示していただきました。これは研究プロジェクトを効率良く進めるためだけではなく、今後の実用化への近道と期待できるものです。このように開発ツールに関する技術的な知見を背景に、AdaCoreはバランスの良いソリューションを提示してくれています」
「コンピュータ・システムならびにソフトウェアの開発のために、モデル指向形式手法の1つであるVDM (Vienna Development Method)を使用しました。」と長崎県立大学の日下部茂教授は語っている。
「VDMモデルの構築と分析は、開発の初期段階から、システム仕様の不完全性とあいまいさを識別することに役立ちます。FFIの実現に向けて、このような既に確立されたソフトウェア向けの形式手法と、近年着目されている俯瞰的な観点のシステムエンジニアリングアプローチを組合わせる研究を行っていました」
FFI（Freedom from Interference）について
自動車メーカーは、ソフトウェアの安全解析を行い、何らかの障害が発生しても安全関連機能を継続して実行することを証明しなければならない。この解析の一部は、FFIオブジェクティブに適合しなければならない。FFIはISO 26262によって求められており、安全上重要な機能と安全性にかかわらない機能が共存する場合、「２個またはそれ以上のエレメントでカスケード故障（障害の連鎖）が発生し、それが安全上の要求を阻害することがあってはならない」とされている。
例えば、自動運転システムを制御するソフトウェアは安全性が最重要であり、ASILが低いコンポーネント（例えばインフォテインメントなど）から保護されなければならない。 FFIはこうした問題に対処する現実的なアプローチだ。
SPARK Proについて
SPARK Proはフォーマルメソッドを用いて完全性を検証する統合型の静的分析ツールスイート。「SPARK 2014」言語をサポートし、GNAT Programming Studio (GPS)ならびに GNATbench IDEに統合された先進的な検証ツールを提供する。
SPARK Proを使うことで、開発者はソフトウェアのアーキテクチャ・プロパティを形式化して定義でき、自動的にそれらを検証できる。それによって、ソフトウェアの完全性を広く保証できる。
例えば、ランタイムエラーの防止、セキュリティポリシーの強制、機能の正確性（形式化して定義された仕様に準拠していること）など。この自動検証は、ソフトウェアの障害が許容されないアプリケーションに特に適している。SPARK Proはコストと開発期間を削減するのを助け、フォーマルメソッドの使用によって数学的検証方法でソフトウェアライフサイクルの早い段階で問題を防ぎ、検出し、取り除く。SPARK言語とツールは、最も要求の高いセーフティ・クリティカルかつ高セキュリティのシステムで多くの採用実績がある。