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: 
Abstract: 
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.
Venue: 
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
bibtex: 
@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 }