Verification of mathematical design documents

The problem to be studied in this thesis is how to verify a set of mathematical design documents in the sense that if each component is implemented correctly, the whole system should work together harmoniously to satisfy the system requirements. In general, a software modular design is often a procedure of 1) decomposition of a complex system into manageable modules that can be developed seperately, 2) specifying and developing each component individually, and 3) combining the components back into a system. The collection of software components that is aimed at finishing a required task together must cooperate with each other through some communication paths. We consider the interconnection description of such a collection of software components as an integral part of a software design. In this thesis, we present an approach to a) describing a network of components, b) checking whether the network is completely connected and whether it is consistent, i.e., whether the components can work together properly, c) determining the behaviour of the network, i.e., what the components will do if they are combined together as described in the network description, and d) checking whether the behavior of the network conforms to the requirements, i.e., if the network behaves as required. We have shown how to determine the behavior of a network of components from the description of the internal structure and the behavioral description of each component, established the conformance relation for checking the correctness of a design, and presented a procedure for checking the consistency and correctness of a set of fully specified components on the basis of their interface descriptions and a description of the way in which the components are connected. Three case studies are presented to illustrate how the approach works. In these case studies, the following steps are included: specifying the system requirements, decomposing the system, describing the behavior of each component, defining their interconnections, followed by a completeness and consistency checking of the component network as well as the derivation of the network behaviour and the correctness checking of this design before investing time in building the components. In the approach developed in this thesis, each component is viewed as a hardware-like device in which the value of an output variable can change instantaneously when input values change and all components operate synchronously rather than in sequence. The connections among components are through shared variables. The behavioural requirements for the software are described by a representation of the relation between the history of input and output values and the current value of the output variables. The behavioural description of the network is derived by using classical relation composition; and the conformance relation is defined using mathematical concepts and standard mathematical logic. Therefore the approach is fully mathematic-based and can be implemented automatically.