Checking Relational Specifications With Binary Decision Diagrams

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

Proc. Foundations of Software Engineering 96

Abstract

Checking a specification in a language based on sets and relations (such as Z) can be reduced to the problem of finding satisfying assignments, or models, of a relational formula. A new method for finding models using ordered binary decision diagrams (BDDs) is presented that appears to scale better than existing methods.

Relational terms are replaced by matrices of boolean formulae. These formulae are then composed to give a boolean translation of the entire relational formula. Thoughout, boolean formulae are represented with BDDs; from the resulting BDD, models are easily extracted.

The performance of the BDD method is compared to our previous method based instead on explicit enumeration. The new method performs as well or better on most of our examples, but can also handle specifications that, until now, we have been unable to analyze.

Keywords:

model checking, binary decision diagrams, relational calculus, formal specification, Z.

Back to Nitpick Home Page