• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

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

Research Project

Project/Area Number 20K19773
Research Category

Grant-in-Aid for Early-Career Scientists

Allocation TypeMulti-year Fund
Review Section Basic Section 60050:Software-related
Research InstitutionJapan Advanced Institute of Science and Technology

Principal Investigator

冨田 尭  北陸先端科学技術大学院大学, 情報社会基盤研究センター, 准教授 (80749226)

Project Period (FY) 2020-04-01 – 2025-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥1,690,000 (Direct Cost: ¥1,300,000、Indirect Cost: ¥390,000)
Fiscal Year 2021: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000)
Keywordsソフトウェア工学 / 形式手法 / 確率・統計 / モデルベース開発 / 電子制御モデル
Outline of Research at the Start

本研究の目的は,実際のモデルベース開発現場に応用可能なモデルテスト自動生成の基盤技術を開発することである.具体的には,産業界の実際の実装モデルを研究対象とし,高い判定・条件・MC/DC カバレッジを達成するテストスイート自動生成手法の開発を行う.
基本的な方針として,乱択探索技術(モンテカルロ法)とテンプレートベース手法(ヒューリスティックの一種)を組み合わせた既存手法を基に,軽量な形式的解析手法と確率・統計的手法を更に導入することで,カバレッジ及び生成効率の向上を目指す.本研究では,共同研究先企業の協力の下,実際の開発現場のフィードバックを受けながら研究を進める.

Outline of Annual Research Achievements

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

Current Status of Research Progress
Current Status of Research Progress

4: Progress in research has been delayed.

Reason

コロナ禍における所属部署(情報社会基盤研究センター)の業務が大幅増加等による全体的な進捗の遅れを取り戻せていないため.

Strategy for Future Research Activity

今後は,まず,定数伝播解析技術及び並列化手法の成果を論文としてまとめる.また,より高度なデータフロー解析や,SAT/SMTソルバ等の技術/ツールを活用し 非保存的近似等を利用したテストケース生成手法の検討・実装を進める.

Report

(4 results)
  • 2023 Research-status Report
  • 2022 Research-status Report
  • 2021 Research-status Report
  • 2020 Research-status Report
  • Research Products

    (3 results)

All 2022

All Presentation (3 results) (of which Int'l Joint Research: 3 results)

  • [Presentation] SMT-Based Model Checking of Industrial Simulink Models2022

    • Author(s)
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Ngoc Thi Bich Do, Hideaki Takai
    • Organizer
      20th International Conference on Software Engineering and Formal Methods
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research
  • [Presentation] Coverage Testing of Industrial Simulink Models using Monte-Carlo and SMT-Based Methods2022

    • Author(s)
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki, The Quyen Ngo, Thi Bich Ngoc Do, Hideaki Takai
    • Organizer
      22nd IEEE International Conference on Software Quality, Reliability and Security
    • Related Report
      2022 Research-status Report
    • Int'l Joint Research
  • [Presentation] Approximate Translation from Floating-Point to Real-Interval Arithmetic2022

    • Author(s)
      Daisuke Ishii, Takashi Tomita, Toshiaki Aoki
    • Organizer
      NASA Formal Methods 2022
    • Related Report
      2021 Research-status Report
    • Int'l Joint Research

URL: 

Published: 2020-04-28   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi