Faster Checking of Software Specifications By Eliminating Isomorphs
Authors: Daniel Jackson and Somesh Jha
Postscript or PDF
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.
model checking, symmetry, relational calculus, formal specification, Z.
Software Systems Research Group in the School
of Computer Science at Carnegie Mellon
[Last modified 19-Feb-1999.
Mail suggestions to the Maintainer.]