Skip to main content
U.S. flag

An official website of the United States government

Official websites use .gov
A .gov website belongs to an official government organization in the United States.

Secure .gov websites use HTTPS
A lock ( ) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.

Using Model Checking to Generate Tests From Specifications

Published

Author(s)

P E. Ammann, Paul E. Black, William J. Majurski

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 output. 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, the generation of test cases is automatic; each counterexample serves as a complete test case. Second, in sharp contrast to program-based mutation analysis, the identification of equivalent mutants is also automatic; the model checker simply reports that the mutant satisfies the constraints, and hence no counterexample is produced. We apply our method to an example specification and evaluate the resulting test sets with coverage metrics on a corresponding implementation in Java.
Conference Dates
December 1, 1998
Conference Location
Brisbane, 1, AS
Conference Title
IEEE International Conference on Formal Engineering Methods

Keywords

formal specification, Java, model checking, test generation

Citation

Ammann, P. , Black, P. and Majurski, W. (1998), Using Model Checking to Generate Tests From Specifications, IEEE International Conference on Formal Engineering Methods, Brisbane, 1, AS (Accessed May 19, 2024)

Issues

If you have any questions about this publication or are having problems accessing it, please contact reflib@nist.gov.

Created October 31, 1998, Updated October 12, 2021