University of Minnesota
Software Engineering Center

You are here

Coverage Based Test-Case Generation using Model Checkers

Date of Publication: 
April 2001
Associated Research Groups: 
Publication Files: 
This paper presents a method for automatically generating test cases to structural coverage criteria. We show how a model checker can be used to automatically generate complete test sequences that will provide a predefined coverage of any software development artifact that can be represented as a finite state model. Our goal is to help reduce the high cost of developing test cases for safety-critical software applications that require a certain level of coverage for certification, for example, safety-critical avionics systems that need to demonstrate MC/DC (modified condition and decision) coverage of the code. We define a formal framework suitable for modeling software artifacts, like, requirements models, software specifications, or implementations. We then show how various structural coverage criteria can be formalized and used to make a model checker provide test sequences to achieve this coverage. To illustrate our approach, we demonstrate, for the first time, how a model checker can be used to generate test sequences for MC/DC coverage of a small case example.
IEEE International Conference on the Engineering of Computer Based Systems, Washington DC, April 2001.
@INPROCEEDINGS{TestGeneration:ECBS01, author = {Sanjai Rayadurgam and Mats P.E. Heimdahl}, Title = {Coverage Based Test-Case Generation Using Model Checkers}, booktitle ={Proceedings of the 8th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS 2001)}, Year = {2001}, Month = {April}, Pages = {83--91}, Publisher = {IEEE Computer Society} }