Automatic Test Generation with Model Checking Techniques
01 January 2006
Formal verification is becoming a key technology to ensure the qualilty of complex (hardware/software) systems. As today formal verification is widely used in the hardware design phase, it is more or less neglected in software or even systems development. In this document we describe a method to automatically generate automated test cases using an abstract system description in combination with a model checking tool. The abstract system description can be used to generate hardware/software systems and the generated test cases might also be reused to verify the correctness of this implementation.