Computer Science Department
School of Computer Science, Carnegie Mellon University
Craig A. Damon
Keywords: Relational calculus, exhaustive search, model checking,
specification checking, constraint satisfaction
Selective enumeration is an approach to pruning search trees with the
goal of preventing the generation of extraneous paths in the search tree,
rather than generating paths that will later be pruned. The reduction in
the size of the search tree scales exponentially with both the number
of variables and the number of values, making complete coverage of
very large (in excess of 1e100 nodes) search trees tractable.
This dissertation demonstrates that selective enumeration enables
an analysis of formal specifications of software systems. This
analysis discovers counterexamples to user-defined claims about
properties of a specification by solving formulae derived the
specification. Ladybug is a new tool that incorporates selective
enumeration to check software designs. Ladybug's input language is
essentially a first-order subset of Z, one of the most broadly used
software specification languages.
Ladybug includes implementations of three significant new algorithms to
help reduce the search space: bounded generation, domain coloring, and
isomorph-eliminating relation generators. Bounded generation improves
upon traditional tree pruning techniques by preventing the generation
of many subtrees that would subsequently be eliminated. Domain coloring
provides an efficient means of building a sound approximation to the
automorphism group of an assignment. The isomorph-eliminating generators
yield a nearly perfect superset of an isomorph-free set of assignments
with minimal cost.
In this thesis, I have applied Ladybug to a suite of software
specifications, including both artificial and "real-world" specifications,
to quantify the success and failure of Ladybug at analyzing software
specifications. I have also used Ladybug as part of a larger case
study examining portions of the DoD High Level Architecture specification.