Although testing has been widely recognized as a practical means of establishing that the software meets its intended purpose, it is an extremely costly and time consuming process.
Model checking is proposed as an automatic verification technique to analyze whether a system model satisfies the system properties. However, we are interested in its capability to generate counterexamples as well as its verification function. Our concern is how model checking be employed in automatic generation of test cases.
In this thesis, we apply model checking technique to control-flow and data-flow oriented test case generation from SDL specification. And we developed a test generation environment which supports the automatic test case generation from SDL specification using the model checker SMV. The SDL specification translated into the form of model checker’s input using a flowgraph as an intermediate process. Then the properties are generated using the control flow and data flow information of the SDL to force the SMV to generate counterexamples. Then test suites are generated by analyzing counterexamples.
