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

MPE Heimdahl, S Rayadurgam, W Visser… - … Workshop on Formal …, 2003 - Springer
MPE Heimdahl, S Rayadurgam, W Visser, G Devaraj, J Gao
International Workshop on Formal Approaches to Software Testing, 2003Springer
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 …
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− 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.
Springer
顯示最佳搜尋結果。 查看所有結果