Generating Efficient Test Sets with a Model Checker

---

Presented at SEFM 04, Beijing, China, September 2004; appears in the proceedings published by IEEE, pp. 261-270.

Authors

Gregoire Hamon, Leonardo de Moura, and John Rushby

Abstract

It is well-known that counterexamples produced by model checkers can provide a basis for automated generation of test cases. However, when this approach is used to meet a coverage criterion, it generally results in very inefficient test sets having many tests and much redundancy. We describe an improved approach that uses model checkers to generate efficient test sets. Furthermore, the generation is itself efficient, and is able to reach deep regions of the statespace. We have prototyped the approach using the model checkers of our SAL system and have applied it to model-based designs developed in Stateflow. In one example, our method achieves complete state and transition coverage in a Stateflow model for the shift scheduler of a 4-speed automatic transmission with a single test case.

Download: PS, PDF

BibTeX Entry

@inproceedings{HdeMR04,
        AUTHOR = {Gr\'{e}goire Hamon and Leonardo de Moura and John Rushby},
        TITLE = {Generating Efficient Test Sets with a Model Checker},
        BOOKTITLE = {2nd International Conference on Software Engineering and Formal Methods},
        ADDRESS = {Beijing, China},
        ORGANIZATION = {IEEE Computer Society},
        PAGES = {261--270},
        MONTH = sep,
        YEAR = 2004
} 

Examples

Scheme Script

Paste this into sal-sim (you need SAL Version 2.3 or later): testgen.scm

Stopwatch

SAL file: stopwatch.sal

Shift Scheduler

Matlab file: trans_ga2.mdl
SAL translation: trans_ga2.sal (we are in the process of improving the translator)
Test translated back: trans_ga2_test.txt

Flight Guidance System

SAL file: ToyFGS05_Left.sal
Test goals: ToyFGS05_Left_goals.scm

Slides

These are from a talk given at the National Institute of Aerospace, Hampton VA on 26 July 2004.
PS, PDF

---

Leonardo de Moura: demoura@csl.sri.com