Automatic test case generation from Simulink/Stateflow models using model checking

摘要

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.