Complementary Criteria for Testing Temporal Logic Properties

摘要

While traditional testing can give evidence that an implementation conforms to a specification there is no guarantee that the implementation therefore also satisfies user requirements. Consequently, it is useful to derive test cases also from requirement properties. In this paper we introduce two new test criteria to measure adequacy of existing test suites and to derive test cases with regard to requirements formalized in linear temporal logic (LTL). The first criterion is complementary to existing criteria for requirement properties in that it focuses on cases where literals in a property should not affect the outcome of the property. The second criterion uses mutation to measure the sensitivity of a test suite with regard to the implemented requirements. In addition to coverage measurement these criteria can also be used to automatically create coverage adequate test suites with a model checker. The results of a case study illustrate the feasibility of the new criteria and demonstrate that they complement existing criteria.