全2296文字

 車載ソフトの欠陥(バグ)をゼロにする開発手法が注目を集めている。自動運転を背景に、ソフトの安全性やセキュリティーをこれまで以上に高める必要性が出てきたためだ。トヨタ系で電動パワーステアリング(EPS)大手のジェイテクトが量産に導入しようとしているほか、自動運転向けの車載SoC(System on Chip)を手掛ける米NVIDIA(エヌビディア)も同様の手法を検討している。

 ジェイテクトやエヌビディアが検討しているのは、ソフトに欠陥がないことを数学的に証明する「定理証明(形式手法の一種)」と呼ぶものだ。自動運転やステアバイワイヤ(SBW)の実用化に伴い、車載ソフトの安全要求は急激に高まっている。これまではシステムの主機能に故障が発生した場合、安全機構によってシステムを停止すれば済んでいた。これに対し、自動運転やSBWではシステムを停止するとむしろ危険なため、安全機構によって最低限の機能(バックアップ機能)を継続する必要がある。

自動運転やSBWを背景に安全要求が変化
自動運転やSBWを背景に安全要求が変化
(出所:ジェイテクト)
[画像のクリックで拡大表示]

 ところが、こうした安全機構の実装は、「困難な場合もある」(ジェイテクト ステアリング事業本部先行システム開発部の米木真哉氏)という。通常、安全機構には主機能とは異なる実装形態のソフトを組み込む。しかし、EPSの場合は主機能も安全機構も、同じ入力に対して同じ出力を返す必要があり、ソフトの実装形態を変えることが難しい。このため、安全機構がなくても、主機能だけで問題がないことを証明する手法を同社は探していた。

 通常、車載ソフトの安全性はテスト工程で検証する。ただ、欠陥がないことを証明することは難しい。テスト条件は無数にあり、どれほど網羅性を高めたとしても、欠陥がないとは言い切れない。そのため、最終的に安全かどうかは顧客が判断することになる。これに対し、定理証明では数学的にソフトの欠陥がゼロであることを証明できる。「誰もが納得できる判断材料として使える可能性がある」(同氏)という。