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

电控模型验证中形式方法与概率/统计方法的融合

• 批准号: 20K19773
• 负责人: 冨田 尭
• 金额: $ 2.75万
• 依托单位: Japan Advanced Institute of Science and Technology
• 依托单位国家: 日本
• 项目类别: Grant-in-Aid for Early-Career Scientists
• 财政年份: 2020
• 资助国家: 日本
• 起止时间: 2020-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://kaken.nii.ac.jp/en/grant/KAKENHI-PROJECT-20K19773/
• 关键词: ソフトウェア工学; 形式手法; 確率・統計; モデルベース開発; 電子制御モデル

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

This study aims to develop international standards ISO26262 and DO-178C/ED-12C, and to determine the criteria for MC/DC standard development. It focuses on the automatic generation of high performance standards to achieve high performance standards. It also aims to jointly study the development of practical substrate technology for enterprises. Explore the development and implementation of spatial efficiency analysis techniques, and jointly study the cooperation elements of advanced enterprises. The fixed number analysis technology is used to analyze the set of candidate points for the function change of the image. The industry has created a system for comparing and calculating the number of fixed numbers in the calculation loop, and the candidate for the function change point of the effect is selected, and the generation of the effect rate is displayed. In addition, the utility of existing SAT/SMT solutions and other technologies in the development of new technologies was confirmed. In 2021, we will review the suitability analysis method of the project and confirm the improvement of the function and performance. Parallel technology trial implementation in 2022, large-scale parallel computer implementation parallel technology implementation, the use of a large number of computing resources, the time to generate a significant increase in the number of The usefulness of SAT/SMT solutions in the development and implementation of technologies such as satellite generation and connectivity was confirmed.

项目成果

Coverage Testing of Industrial Simulink Models using Monte-Carlo and SMT-Based Methods

• DOI: 10.1109/qrs57517.2022.00050
• 发表时间: 2022-12
• 期刊: 2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)
• 作者: Daisuke Ishii;Takashi Tomita;Toshiaki Aoki;T. Ngo;Thi Bich Ngoc Do;Hideaki Takai

SMT-Based Model Checking of Industrial Simulink Models

基于 SMT 的工业 Simulink 模型模型检查

• DOI: 10.1007/978-3-031-17244-1_10
• 发表时间: 2022
• 期刊: Proc. 23rd International Conference on Formal Engineering Methods (ICFEM)
• 作者: Daisuke Ishii;Takashi Tomita;Toshiaki Aoki;The Quyen Ngo;Thi Bich Ngoc Do;Hideaki Takai
• 通讯作者: Hideaki Takai

Approximate Translation from Floating-Point to Real-Interval Arithmetic

从浮点运算到实数区间运算的近似转换

• DOI: 10.1007/978-3-031-06773-0_39
• 发表时间: 2022
• 期刊: Proc. NASA Formal Methods
• 作者: Daisuke Ishii;Takashi Tomita;Toshiaki Aoki
• 通讯作者: Toshiaki Aoki