トヨタ系やNVIDIAが注目、数学的に欠陥ゼロのソフト開発

車載ソフトの欠陥（バグ）をゼロにする開発手法が注目を集めている。自動運転を背景に、ソフトの安全性やセキュリティーをこれまで以上に高める必要性が出てきたためだ。トヨタ系で電動パワーステアリング（EPS）大手のジェイテクトが量産に導入しようとしているほか、自動運転向けの車載SoC（System on Chip）を手掛ける米NVIDIA（エヌビディア）も同様の手法を検討している。 ジェイテクトやエヌビディアが検討しているのは、ソフトに欠陥がないことを数学的に証明する「定理証明（形式手法の一種）」と呼ぶものだ。自動運転やステアバイワイヤ（SBW）の実用化に伴い、車載ソフトの安全要求は急激に高まっている。これまではシステムの主機能に故障が発生した場合、安全機構によってシステムを停止すれば済んでいた。これに対し、自動運転やSBWではシステムを停止するとむしろ危険なため、安全機構によって最低限の機能（バ

[pascal256]

形式手法は普通の業務ロジックに応用するのはコスパが悪そうな印象だけど、自動運転とかには確かに良いのかも。SPINとかAlloyで止まってたけどSpark言語ってのもあるのね。しかしなぜにAdaベース？？？

[gui1]

「欠陥ゼロ」　←　フラグたてんなヽ(｀Д´#)ﾉ

[reboot_in]

“ジェイテクトやエヌビディアが検討しているのは、ソフトに欠陥がないことを数学的に証明する「定理証明（形式手法の一種）」と呼ぶものだ。”

[katsusuke]

名古屋の関数型の人たちをトヨタが一網打尽

[chess-news]

同じこと考えるもんだな。