2.5 Applications and Limitations

The simple example of ZD shown above illustrates one of the mechanisms for maintaining the consistency of a functional representation. We have applied this formalism in the context of design rationale capture in the following way: during a top-down design process, a designer proposes a particular decomposition of a system. The details for how each of the parts of this system (represented in ZD as devices) is to be realized has not yet been determined. However, it is possible for the designer to specify some constraints about the fillers of these roles at this time. As other designers on the team work to fill in the particular roles, ZD can automatically verify whether a particular combination of choices is satisfactory, according to the original designer's expressed constraints.

We have demonstrated this apporach on a handful of examples, which have shown that it is applicable to simple configuration problems such as the Year 2000 example shown here, as well as more involved analyses of iterative behavior at both the implementation and architectural description levels. The real limitation in the method seems to be the expressiveness of the finite-state language used to describe the relationships between functional components; our experiments have shown that this limitation is more restrictive than the choice of NQTHM as a theorem prover. The architecture of the ZD implementation was designed so that the theorem prover could be easily exchanged for another; however, we have not found a need to do so. The information available from the functional representation has proven so far to be sufficient to provide the theorem prover enough information to avoid any impasses in its proofs.