欠陥ゼロのソフト開発手法　自動運転の安全要求応える

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

ジェイテクトやエヌビディアが検討しているのは、ソフトに欠陥がないことを数学的に証明する「定理証明（形式手...