Li Tan, Oleg Sokolsky, and Insup Lee. In the proceedings of IEEE Internation Conference on Information Reuse and Integration (IRI'04), Las Vegas, NV, IEEE society, 2004.
This paper considers the specification-based testing in which the requirement is given in the linear temporal logic (LTL). The required LTL property must hold on all the executions of the system. The central piece of our framework is a property-coverage metrics. Based on the requirement mutation, the metrics measures how well a property has been tested by a test suite. We define a coverage criteria based on the metric that selects a finite set of tests from all the possible executions of the system. We also discuss the technique of generating a test suite for specification testing by using the counterexample mechanism of a model checker. By exploiting the special structure of a generated test, we are able to reduce a test with the infinite length to an equivalent one of finite length. Our framework provides a model-checking-assisted approach that generates a test suite that is finite in size and in length for testing linear temporal properties on an implementation.