Paul E. Black, Vadim Okun, and Yaacov Yesha, Mutation of Model Checker Specifications for Test Generation and Evaluation, Mutation Testing for the New Century, proc. of Mutation 2000, San Jose, California (October 2000), edited by W. Eric Wong, Kluwer Academic Publishers, pages 14-20.

    Mutation analysis on model checking specifications is a recent development. This approach mutates a specification, then applies a model checker to compare the mutants with the original specification to automatically generate tests or evaluate coverage. The properties of specification mutation operators have not been explored in depth. We report our work on theoretical and empirical comparison of these operators. Our future plans include studying how the form of a specification influences the results, finding relations between different operators, and validating the method against independent metrics.

Get the paper in DVI (43k), Postscript (83k), or PDF.

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

Updated Wed Jul 10 10:29:33 2002

by Paul E. Black  (

Go to Black's papers or NIST home page.