Exploiting Symmetry in the Model Checking of Relational Specifications

Author: Daniel Jackson

Tecnical Report CMU-CS-94-219.

Sorry, no postscript available.

Abstract

Errors in a software design can be detected early on by analyzing a formal model expressed in a specification language such as Z. Since software designs tend to involve infinite (or at least very big) state spaces, it has been assumed that this analysis cannot be automated. Consequently, few formal specifications have been extensively analyzed, and the potential for early detection of errors has not been realized.

This paper argues that, while proving properties of designs may be intractable, detecting errors may not be. State transitions of an operation can be enumerated exhaustively, within a 'scope' defined by the user that places a bound on the size of state components. Symmetry can then be exploited to reduce this finite state space. A state can be shown to be symmetrical, in the context of the analysis, to a state already examined, and thus guaranteed not to reveal an error.

Preliminary experiments with a prototype are promising. A small scope often seems sufficient to catch errors, and exhibits enough symmetry to reduce search by a factor of 10 or more.

Keywords

Symmetry, model checking, software design, formal specification, Z, relational calculus.