University of Minnesota
Software Engineering Center

You are here

Auto-Generating Test Sequences using Model Checkers: A Case Study

Date of Publication: 
October 2003
Associated Research Groups: 
Use of model-checking approaches for test generation from requirement models have been proposed by several researchers. These approaches leverage the witness (or counter-example) generation capability of model-checkers for constructing test cases. Test criteria are expressed as temporal properties. Witness traces generated for these properties are instantiated to create complete test sequences, satisfying the criteria. State-space explosion can, however, adversely impact model-checking and hence such test generation. Thus, there is a need to validate these approaches against realistic industrial sized system models to learn how well these approaches scale. To this end, we conducted a case study using six models of progressively increasing complexity of the mode-logic in a flight-guidance system, written in the rsml language. We developed a framework for specification-based test generation using the NuSMV model-checker and code based test case generation using Java Pathfinder, and collected time and resource usage data for generating test cases using symbolic, bounded, and explicit state model-checking algorithms. This paper briefly discusses the approach, presents the results from the study and analyzes its implications.
Proceedings of the 3rd International Workshop on Formal Approaches to Testing of Software (FATES 2003)}. Montreal, Quebec, Canada, October 2003. Published as Springer Verlag Lecture Notes In Computer Science 2931
@inproceedings{Heimdahl03:CaseStudyFGS, author = " Mats P.E Heimdahl and S. Rayadurgam and Willem Visser and George Devaraj and Jimin Gao ", title = " Auto-Generating Test Sequences using Model Checkers: A Case Study ", booktitle = " 3rd International Worshop on Formal Approaches to Testing of Software (FATES 2003)", publisher = "", volume = "", year = 2003 }