Paul E. Ammann, Paul E. Black, and William Majurski, Using Model Checking to Generate Tests from Specifications, Proceedings of 2nd IEEE International Conference on Formal Engineering Methods (ICFEM'98), Brisbane, Australia (December 1998), edited by John Staples, Michael G. Hinchey, and Shaoying Liu, IEEE Computer Society, pages 46-54.

Abstract:

    We apply a model checker to the problem of test generation using a new application of mutation analysis. We define syntactic operators, each of which produces a slight variation on a given model. The operators define a form of mutation analysis at the level of the model checker specification. A model checker generates counterexamples which distinguish the variations from the original specification. The counterexamples can easily be turned into complete test cases, that is, with inputs and expected results. We define two classes of operators: those that produce test cases from which a correct implementation must differ, and those that produce test cases with which it must agree.

    There are substantial advantages to combining a model checker with mutation analysis. First, test case generation is automatic; each counterexample is a complete test case. Second, in sharp contrast to program-based mutation analysis, equivalent mutant identification is also automatic. We apply our method to an example specification and evaluate the resulting test sets with coverage metrics on a Java implementation.

20 Year ICFEM Most Influential Paper Award 14 November 2018

Get the paper in DVI (68k), Postscript, gzip'd (50k), Postscript (130k), or PDF (208k).

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

Updated Mon Nov 26 13:56:07 2018

Go to Black's papers or NIST home page.