Auto-generating test sequences using model checkers: A case study

Mats P.E. Heimdahl, Sanjai Rayadurgam, Willem Visser, George Devaraj, Jimin Gao

Research output: Contribution to journalArticlepeer-review

42 Scopus citations


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

Original languageEnglish (US)
Pages (from-to)42-59
Number of pages18
JournalLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
StatePublished - Dec 1 2004


Dive into the research topics of 'Auto-generating test sequences using model checkers: A case study'. Together they form a unique fingerprint.

Cite this