University of Limerick Institutional Repository

Verification of mathematical design documents

DSpace Repository

Show simple item record

dc.contributor.advisor Lorge Parnas, David
dc.contributor.advisor Fitzgerald, Brian Liu, Zhiying 2011-12-06T17:14:52Z 2011-12-06T17:14:52Z 2011
dc.description peer-reviewed en_US
dc.description.abstract 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. en_US
dc.description.sponsorship SFI
dc.language.iso en_US en_US
dc.publisher University of Limerick en_US
dc.subject mathematical design en_US
dc.subject verification en_US
dc.title Verification of mathematical design documents en_US
dc.type Doctoral thesis en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.type.supercollection ul_theses_dissertations en_US
dc.type.restriction none en

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account