Coverage Testing of Industrial Simulink Models using Monte-Carlo and SMT-Based Methods
Coverage Testing of Industrial Simulink Models using Monte-Carlo and SMT-Based Methods
复制标题
DOI：
10.1109/qrs57517.2022.00050
复制
发表时间：
2022-12
期刊：
影响因子：
--
通讯作者：
Daisuke Ishii;Takashi Tomita;Toshiaki Aoki;T. Ngo;Thi Bich Ngoc Do;Hideaki Takai
中科院分区：
文献类型：
--
作者：
Daisuke Ishii;Takashi Tomita;Toshiaki Aoki;T. Ngo;Thi Bich Ngoc Do;Hideaki Takai
Simulink是为网络物理系统建模的流行工具。随着工业上生产的模型越来越多，模型的自动化质量保证变得越来越重要。本文对四种用于Simulink模型覆盖率测试的方法进行了实证评估：A)专用官方工具SLDV；B)基于模板的蒙特卡罗(TBMC)方法，它是一种利用输入信号模板的随机测试生成方法；C)基于SMT的模型检测(SBMC)方法，它通过将模型编码成逻辑公式来进行静态分析；D)B和C的混合方法。在实验中，我们将这些方法应用于14个模型，并对它们的性能进行了评估。结果表明，在多个模型上，混合方法取得了比SLDV更好的结果。
Simulink is a popular tool for modeling cyber-physical systems. As more models are produced in industry, automated quality assurance of models becomes increasingly important. This paper describes an empirical evaluation of four methods for the coverage testing of Simulink models: A) SimuLink Design Verifier (SLDV), a dedicated official tool; B) Template-Based Monte-Carlo (TBMC) method, a random test generation method that utilizes input signal templates; C) SMT- Based Model Checking (SBMC) method that conducts static analysis via encoding models into logic formulas; and D) a hybrid method of B and C. Based on the evaluation results, we carefully designed the hybrid method to complement the features of TBMC and SBMC. In the experiments, we have applied the methods to fourteen models and evaluated their performance. The results show that the hybrid method achieved better results than SLDV for several models.