Faster Checking of Software Specifications By Eliminating Isomorphs

Authors: Daniel Jackson and Somesh Jha

Abstract

Abstract. Both software specifications and their intended properties can be expressed in a simple relational calculus. The claim that a specification satisfies a property becomes a relational formula that can be checked automatically by enumerating the formula's interpretations. Because the number of interpretations is usually huge, this approach has not been thought to be practical. But by eliminating isomorphic interpretations, the enumeration can be reduced substantially, by a factor of k! for each basic type of k elements.

Keywords:

model checking, symmetry, relational calculus, formal specification, Z.

Composable Software Systems Research Group in the School of Computer Science at Carnegie Mellon University.

[Last modified 19-Feb-1999.
Mail suggestions to the Maintainer.]