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

2020 Fiscal Year Research-status Report

• Project/Area Number: 20K19773
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 冨田 尭 北陸先端科学技術大学院大学, 情報社会基盤研究センター, 講師 (80749226)
• Project Period (FY): 2020-04-01 – 2023-03-31
• Keywords: ソフトウェア工学 / 形式手法 / 確率・統計 / モデルベース開発 / 電子制御モデル

Outline of Annual Research Achievements

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

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

コロナ禍において所属部署（情報社会基盤研究センター）の業務が大幅に増加したため，及び，共同研究先企業との連携にも支障をきたしたため，当初の予定通りにエフォートを割くことができなかったため．

Strategy for Future Research Activity

今後は，まずこれまでの成果を論文としてまとめる．また，より高度なデータフロー解析や，SAT/SMTソルバ等の技術/ツールを活用し非保存的近似等を利用したテストケース生成手法の開発を進める．そして，予備実験によりモデル内部のシミュレーションデータを単純に加工するだけで有効なテストケースとして利用できる場合があることが確認されているため，生成済みテストケース候補に対するシミュレーションデータを加工し新たな有望テストケース候補を効率的に生成する手法の開発を行う．

Causes of Carryover

研究進捗の遅れのため．
次年度における国際会議及び国内会議参加のための旅費，プログラム実装のための人件費・謝金，その他学会参加費や論文掲載料等に用いる.