Rayadurgam, SanjaiHeimdahl, Mats2020-12-102020-12-102001IEEE International Conference on the Engineering of Computer Based Systems, Washington DC, April 2001.https://hdl.handle.net/11299/217353Associated research group: Critical Systems Research GroupThis 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.Report