自動車の機能安全を実現するための形式手法への取り組み
AdaCore
TechPaper
自動車業界ではソフトウェアのリコールが増加しており、安全性は今や重要な経営課題となっています。
本稿では、Ada および SPARK が形式的検証を通じて ISO 26262 への準拠を可能にし、欠陥の削減、安全性とセキュリティの強化にどのように貢献するかを解説します。
NVIDIA が SPARK を活用して最高レベルの保証を達成した事例を紹介し、同様の成果を貴社でも実現できる理由をご説明します。


