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.
|Original language||English (US)|
|Number of pages||9|
|State||Published - Jan 1 2001|
|Event||8th Annual IEEE International Conference on the Workshop on the Engineering of Computer Based Systems - Washington, DC, United States|
Duration: Apr 17 2001 → Apr 20 2001
|Other||8th Annual IEEE International Conference on the Workshop on the Engineering of Computer Based Systems|
|Period||4/17/01 → 4/20/01|