The Refinement of Formal Specifications Using Reusable Software Components in Ada95

This thesis documents research that enables formal specifications, written in the specification language Z, to be turned into high level code in fewer steps than other refinement techniques and without the need for formal proof. This method helps to overcome one of the mam stumbling blocks for formal methods, which is the difficulty of creating software from the formal specification. In the main, previous methods have either concentrated on creating an animation or prototype of the specification using functional languages or on converting the abstract structures found in specification into the less abstract structures found in high level programming languages, via a series of lengthy proofs.<br/><br/>The method presented in this thesis uses a different approach. Here, the target language is enriched with the abstract structures and operations available to the formal specification language. This is achieved by the construction of a series of reusable software components that model the main types and operations found in Z. The formal specification can then be translated into executable code by selecting the correct operations from the reusable components to implement each of the Z operations.<br/><br/>The research described in this thesis shows that the method is a viable one. as efficient executable code can be produced very quickly, without the need for formal proof, and with great confidence in its correctness. The components required to do this are available and have been written and constructed in such a way as to allow more complex components to be built from them.

Name dc:type.qualificationname

Doctoral Thesis

Level dc:type.qualificationlevel

Student thesis

Year dc:date.issued

1998

Author dc:creator

• Bale, Stephen

Language dc:language

eng

Identifier

oai:pure.atira.dk:studenttheses/e9d0110d-634d-48b4-9d3e-3026424d1a6e

OAI identifier oai:identifier

oai:pure.atira.dk:studenttheses/e9d0110d-634d-48b4-9d3e-3026424d1a6e