Vadim Okun, Paul E. Black, and Yaacov Yesha, Testing with Model Checker: Insuring Fault Visibility, WSEAS Transactions on Systems, Vol. 2, Issue 1, pages 77-82, January 2003.

Also published on CD-ROM:
Proceedings of 2002 WSEAS International Conference on System Science, Applied Mathematics & Computer Science, and Power Engineering Systems, edited by Nikos E. Mastorakis and Petr Ekel, pages 1351-1356, WSEAS, Rio de Janeiro, Brazil (October 2002).

Abstract:

    To detect a fault in software, a test case execution must enable an intermediate error to propagate to the output. We describe two specification-based mutation testing methods that use a model checker to guarantee propagation of faults to visible outputs. We evaluate the methods empirically and show that they are better than the previous "direct reflection" method.

Get the conference paper in PDF (50k), DVI (36k), Postscript (62k), or RTF (41k).
Get the more complete, NIST-IR 6929, in PDF (202k), DVI (58k), or Postscript (174k).

This page's URL is /~black/Papers/propag2002.html

Updated Mon May 19 16:01:31 2003

Go to Black's papers or NIST home page.