Auto-generating Test Sequences Using Model Checkers: A Case Study

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, a...

• Type: Conference
• Year: 2003
• Where: FATES
• Authors: Mats Per Erik Heimdahl, Sanjai Rayadurgam, Willem Visser, George Devaraj, Jimin Gao
• Keywords: Complete Test Sequences, FATES 2003, Test Cases, Test Generation