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.

229 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by [email protected]