Relational Analysis

Specification is recognized to be a critical phase of development, yet is supported by few tools. An elaboration of Chen's entity-relationship notation called an 'object model' is rapidly becoming a dominant design and specification notation - witness the list of 50 companies backing Rational's submission to the OMG of their object modelling language UML. There's a huge variety of CASE tools for constructing object models, but little analysis is provided beyond simple syntactic checks.

The object model is not a passing fad. Its essence is arguably the 'finite state machine' of data structures. It arises again and again in software development and seems intuitive to practitioners. At the same time, it can be given a formal semantics and thus be made precise and amenable to automatic analysis.

We have developed a relational notation called NP (much like a subset of the Z specification language) that attempts to capture this essence. Most of our effort has been directed towards the design of an accompanying checker. Nitpick is the result of this work. Using a brute force enumeration, it finds counterexamples to properties that are claimed to hold of a specification. A variety of reduction mechanisms prunes the search space so that flaws can often be found even in huge spaces.

There are three key ideas here. First is the choice of language constructs. The relational notation is, like the finite state machine, severely limited in its expressiveness, and yet capable of capturing subtle aspects of many practical problems. Second is the nature of the checking. By searching for small finite counterexamples, an enumerative analysis can work well even on an undecidable problem. Third is the reduction mechanisms, primarily one that relies on the primitive types being uninterpreted, so that consequently, cases that are related by a uniform relabelling of atoms are equivalent. Exploiting this is tricky but gives huge speedups.

Our Nitpick checker has been used in a number of small projects. We have taught MSE students how to express problems with a combination of diagrammatic object models and Nitpick's textual notation; they have applied this approach successfully in class projects and in their year-long studio. We have used Nitpick to explore the undesirable properties of a feature of Microsoft Word's paragraph style mechanism. It exposed a flaw in the proof of correctness accompanying a handoff protocol designed for the new FAA system. We have analyzed some descriptions of architectural styles published by David Garlan and David Notkin of implicit invocation systems, demonstrating how Nitpick generates, automatically, instance architectures that satisfy style constraints but violate expected properties. We have analyzed Dave Johnson's mobile host protocol and shown that the authentication mechanism is in fact required for correctness.

We have also investigated different checking mechanisms. We developed a BDD-based scheme that works spectacularly well on some examples for which the explicit method fails. We are now looking at a scheme based on boolean satisfaction algorithms that should handle more complex specifications.

Brought to you by the Composable Software Systems research group at Carnegie Mellon University's School of Computer Science. Last updated Wed Apr 23, 1997.