Testing with Model Checker: Insuring Fault Visibility

Published: January 05, 2003


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.
Citation: WSEAS Transactions on Systems
Volume: 2
Issue: 1
Pub Type: Journals

Download Paper


formal methods, model checking, specification-based testing, mutation testing
Created January 05, 2003, Updated February 19, 2017