#
Isomorph-free Model Enumeration

**Authors:**Daniel Jackson, Somesh Jha, and Craig A. Damon
ACM Transactions on Programming Languages and Systems, Volume 20, No.
2, March 1998, pp. 302-343.

Download the PostScript.

##
Abstract

Software specifications often involve data structures with huge numbers
of values, and consequently cannot be checked using standard state exploration
or model checking techniques. Data structures can be expressed with binary
relations, and operations over such structures can be expressed as formulae
involving relational variables. Checking properties such as preservation
of an invariant thus reduces to determining the validity of a formula,
or, equivalently, finding a model (of the formula's negation).
A new method for finding relational models is presented. It exploits
the permutation invariance of models-if two interpretations are isomorphic,
then neither is a model or both are-by partitioning the space into equivalence
classes of symmetrical interpretations. Representatives of these classes
are constructed incrementally by using the symmetry of the partial interpretation
to limit the enumeration of new relation values. The notion of symmetry
depends on the type structure of the formula; by picking the weakest typing,
larger equivalence classes (and thus fewer representatives) are obtained.
A more refined notion of symmetry that exploits the meaning of the relational
operators is also described. The method typically leads to exponential
reductions, often of 6 orders of magnitude, making the automatic analysis
of relational specifications possible for the first time.

###
Keywords:

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

Back
to Nitpick Home Page