デンソーが長崎県立大との自動車プロジェクトでSPARKを採用

米国のAdaCoreは、株式会社デンソー向け研究プロジェクト「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をパートナーとして選んだ。

プロジェクトのフェーズ1ではAdaCoreと長崎県立大学はFFIの問題点についての調査を行いました。長崎県立大学のチームはフォーマルメソッドの使用について分析し、SPARKのアプローチによってシステムの安全性の検証作業を大幅に簡素化できると判断した。


SPARK Proはフォーマルメソッドを用いて完全性を検証する統合型の静的分析ツールスイート。「SPARK 2014」言語をサポートし、GNAT Programming Studio (GPS)ならびに GNATbench IDEに統合された先進的な検証ツールを提供する。

SPARK Proを使うことで、開発者はソフトウェアのアーキテクチャ・プロパティを形式化して定義でき、自動的にそれらを検証できる。それによって、ソフトウェアの完全性を広く保証できる。

例えば、ランタイムエラーの防止、セキュリティポリシーの強制、機能の正確性（形式化して定義された仕様に準拠していること）など。この自動検証は、ソフトウェアの障害が許容されないアプリケーションに特に適している。

SPARK Proは、コストと開発期間を削減するのを助け、フォーマルメソッドの使用によって数学的検証方法でソフトウェアライフサイクルの早い段階で問題を防ぎ、検出し、取り除く。

SPARK言語とツールは、最も要求の高いセーフティ・クリティカルかつ高セキュリティのシステムで多くの採用実績があるという。（慶尾六郎）

---