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

TLDR

Model‑based test generation using random input or guided simulation falls short of the high coverage and completeness required for safety‑critical systems, while model‑checking‑based techniques have been reported to bridge this gap. The study evaluates the effectiveness of model‑checking‑based test generation by developing the AutoMOTGen tool suite for Simulink/Stateflow and applying it to real‑life case studies at General Motors. AutoMOTGen’s methodology is described and compared with a commercial random input‑based test generation tool on the same set of examples. The results show that model‑checking‑based techniques complement random input‑based methods in coverage, provide unreachability proofs that aid debugging, and are recommended to enhance model‑based testing in safety‑critical systems. © 2013 John Wiley & Sons, Ltd.

Abstract

SUMMARY 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.