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.
Citation: WSEAS Transactions on Systems
Pub Type: Journals
formal methods, model checking, specification-based testing, mutation testing