電子制御モデル検証における形式手法と確率・統計的手法の融合

点击翻译按钮获取中文摘要

本研究では，開発国際標準であるISO26262及びDO-178C/ED-12Cが求める判定・条件・MC/DCカバレッジ基準に注目し，高カバレッジを達成するテストスイートを効率的に自動生成する手法について共同研究先企業から実用的モデルの提供を受け，実践的な基盤技術の開発に取り組んだ．2020年度は，探索空間を効率的に絞り込む手法として定数伝播解析技術を開発・実装し，共同研究先企業の協力の元，実際の産業用モデルでもテストスイートのカバレッジ・生成効率が向上することを確認した．定数伝播解析技術では，テスト対象ブロックにどのような定数値が伝播し得るか，また，それが入力までどのように逆伝播し得るかを分析することで，テスト対象ブロックの機能変化点の候補の集合を得ることができる．産業界で作成される実装モデルでは比較演算や数値演算回路の中で定数が多用されているため，効果的に機能変化点の候補を絞り込み，カバレッジに寄与するテストケースを効率的に生成できることが示された．また，既存のSAT/SMTソルバ等の技術/ツールの活用によるデッドロジック検出技術の開発検討も行い，その有用性を確認した．そして，テスト項目への適合度分析方法の検討・実装を行い，テスト項目に合致する可能性が高いと見込めるテストケースほど高い確率で生成できることが産業用モデルでも確認できた．2021年度は，各種技術の洗練及び対応ブロックの拡充し，機能・性能の向上を確認した．並列化手法の試作を行った．2022年度は，大型並列計算機で実行可能な並列化手法を実装し，多量の計算資源を利用することでテストケース生成の時間効率を大幅に向上させることができることを確認した．また，SAT/SMTソルバ等の技術/ツールの活用によるテストケース生成との連携技術等の開発・実装も行い，その有用性を確認した．