なぜeSOL はTrustInSoft Analyzer採用したのか
～形式検証とASIL D対応を実現したeMCOS POSIXの開発～

自動車や産業機器向けソフトウェアでは、高度化・複雑化が進む一方で、ISO 26262をはじめとする機能安全規格への対応が求められています。特にASIL Dレベルでは、高品質なソフトウェアだけでなく、その品質を証明するための検証エビデンスの整備が不可欠です。

しかし、大規模かつ複雑なRTOSにおいて、膨大なテストやトレーサビリティを効率的に構築しながら、厳格な安全認証要件を満たすことは容易ではありません。

本資料では、eSOLがTrustInSoft Analyzerを活用し、抽象解釈に基づく形式検証をeMCOS POSIXへ適用することで、ISO 26262 ASIL D対応に必要な検証エビデンスをどのように構築したのか、その取り組みと成果を詳しく解説します。

• eSOL eMCOS
• 課題
• 検証プロセスのさらなる課題
• 解決案の検討：AI
• TrustInSoft Analyzer
• TIS Analyzer の適用プロセス
• 適用の結果
• 今後の展望