Testing with Model Checker: Insuring Fault Visibility
Vadim Okun, Paul E. Black, Yelena Yesha
To detect a fault in software, a test case execution must be chosen so intermediate errors propagate to the output. We describe two modeling methods for specification-based mutation testing using model checkers that guarantee this propagation. We evaluate the methods empirically and show that they yield more useful tests than the previous "direct reflection" methods.