Abstract
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) |
---|---|
Pages | 83-91 |
Number of pages | 9 |
State | Published - 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
Other | 8th Annual IEEE International Conference on the Workshop on the Engineering of Computer Based Systems |
---|---|
Country/Territory | United States |
City | Washington, DC |
Period | 4/17/01 → 4/20/01 |