Testing with Model Checker: Insuring Fault Visibility
Vadim Okun, Paul E. Black, Yaacov Yesha · 2003
Abstract:- To detect a fault in software, a test case execution must enable an intermediate error to propagate to the output. We describe two specificationbased mutation testing methods that use a model checker to guarantee propagation of faults to the visible outputs. We evaluate the methods empirically and show that they are better than the previous "direct reflection " approach. Key-Words:- formal methods; model checking; SMV; software engineering; specification-based testing; state machines; test case generation; fault-based testing; mutation testing 1 Introduction Specification-based testing is a black-box technique, that is, it assumes that internal states of the program implementing the specification are unknown, hence failures can only be detected in external responses. Although model checkers can be used to generate tests [3, 6, 10, 13, 25, 17], existing methods allow the model checker to choose tests that do not cause faults to propagate to the program's output. Goradia [16] presents typical cases that prevent a fault in an intermediate state from propagating to the output.