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

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

• 批准号: 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ソルバ等の技術/ツールの活用によるテストケース生成との連携技術等の開発・実装も行い，その有用性を確認した．

在这项研究中，我们专注于国际开发标准ISO26262和DO-178C/ED-12C所需的判断，条件和MC/DC覆盖标准，并从我们的联合研究公司获得了有关自动生成可实现高覆盖范围的测试套件的方法，并在开发实用的基础技术方面进行了实用。在2020财年，开发并实施了不断的传播分析技术，以有效地缩小搜索空间的范围，并且在联合研究公司的合作下，我们确认即使在实际的工业模型中，也可以提高测试套件的覆盖范围和发电效率。借助恒定的传播分析技术，可以通过分析恒定值可以传播到测试块以及如何将它们反向传播到输入中来获得一组候选功能变化点。由于常数经常用于行业中创建的实施模型中的比较和数值算术电路，因此已证明它可以有效地缩小候选人的功能变化点，并有效地生成有助于覆盖范围的测试用例。我们还通过利用现有的SAT/SMT求解器以及其他技术和工具来研究了死亡逻辑检测技术的开发，并确认了其有用性。然后，我们检查并实施了一种分析测试项目适应性的方法，并且也证实，测试用例可能与测试项目相匹配的概率越高，生成的测试案例的概率越高。在2021财年，我们确认了各种技术的完善，并使用兼容块的扩展来改善功能和性能。我们创建了并行化方法的原型。在2022财年，我们确认可以实现大型并行计算机执行的并行化方法，并且通过利用大量计算资源，可以显着提高测试案例案例生成的时间效率。此外，我们已经开发了和实施技术来通过使用SAT/SMT求解器等技术/工具来创建测试案例，并确认了它们的实用性。

项目成果

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