Evolution and reuse of formal specifications using decision structures

In this paper, we discuss the use of knowledge structure, called the decision space, for the evolution of formal specifications. Because evolution is a particularly intense form of reuse, what we say will also impact on reusability. We demonstrate our approach using a formal specification, written in the Z formal specification language, for an aerospace application known as the RSDIMU (Redundant Strapped Down Inertial Measurement Unit). We show that articulating the decision structure and associating it with the artifact produced can be used in the subsequent evolution of the specification. We propose a representation which separates domain knowledge into a decision/issue space and an object space and the solution space into object instances, Z schemas and resolved issues, We show the effect of several changes to the RSDIMU specification and demonstrate how different methods of resolving an issue change the focus of attention within the specifications