Automatic test case generation from Simulink/Stateflow models using model checking
Automatic test case generation from Simulink/Stateflow models using model checking
复制标题
DOI：
10.1002/stvr.1489
复制
发表时间：
2014-03
期刊：
影响因子：
--
通讯作者：
S. Mohalik;Ambar A. Gadkari;Anand Yeolekar;K. Shashidhar;S. Ramesh
中科院分区：
文献类型：
--
作者：
S. Mohalik;Ambar A. Gadkari;Anand Yeolekar;K. Shashidhar;S. Ramesh
基于随机输入生成和引导模拟的基于模型的测试生成技术不能满足安全关键应用所要求的高测试覆盖率和完整性保证的需求。最近，基于模型检测的测试生成技术已被报道，以弥补这一差距。为了评估这些技术的有效性，为Simulink/Stateflow开发了一个内部工具套件AutoMOTGen，并将其应用于通用汽车公司的真实的案例研究。本文概述了AutoMOTGen的测试生成方法，并在同一组示例上与商业的、主要基于随机输入的测试生成工具进行了比较研究。结果表明，在覆盖率方面，基于模型检查的技术补充了基于随机输入的技术。此外，它们还提供了不可达性的证明，这有助于调试模型。因此，建议使用基于模型检查的工具来补充和增强安全关键系统工程中基于模型的测试方法的有效性。版权所有© 2013约翰威利父子有限公司.
Model‐based test generation techniques based on random input generation and guided simulation do not satisfy the demands of high test coverage and completeness guarantees as required by safety‐critical applications. Recently, test generation techniques based on model checking have been reported to bridge this gap. To evaluate the effectiveness of these techniques, an in‐house tool suite, AutoMOTGen, has been developed for Simulink/Stateflow and applied on real‐life case studies at General Motors. This paper outlines the test generation methodology of AutoMOTGen and gives a comparative study with a commercial, primarily random input‐based, test generation tool on the same set of examples. The results indicate that in terms of coverage, model checking‐based techniques complement the random input‐based techniques. In addition, they provide proofs for unreachability that can aid in debugging the models. Therefore, it is recommended that model checking‐based tools be utilized to complement and enhance the effectiveness of model‐based testing methods in safety‐critical systems engineering. Copyright © 2013 John Wiley & Sons, Ltd.