Property relevant software testing with model-checkers

Verification is applied to software as a proof method with respect to its requirements. Software testing is necessary due to the fact that verification is often infeasible. Automation is desirable since the complexity and the effort involved are significant. However, auto-mated software testing is commonly used to ensure confidence in the conformance of an implementation to an abstract model, not to its requirement properties. In this paper, we introduce the notion of property relevance of test-cases. Property relevant test-cases can be used to determine property violations. It is shown how to detect the properties relevant to a test-case. New coverage criteria based on property relevance are introduced. Automated generation of test-suites satisfying these criteria is also presented. Finally, feasibility is illustrated with an empirical evaluation