Isomorph-free Model Enumeration

Authors:Daniel Jackson, Somesh Jha, and Craig A. Damon

Submitted for publication.

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