Writing and animating Z specifications.

The work presented in this thesis is concerned with the issues involved in writing and demonstrating formal specifications of information systems written in Z. The use of Z in software development, to enhance productivity and improve software quality, is not without its problems. Whilst the notation itself is highly developed, ways of systematically using Z to create specifications are, by contrast, poorly documented. Also, given that most commissioners of software are not skilled in reading Z, ways of demonstrating the important features of a formal Z specification to a customer are needed if the effective validation of the specification against user requirements is to take place. In this thesis we present a systematic approach, known as OPERATOR, for developing Z specifications and evaluate it against the issues identified for writing formal specifications. We also look at various ways of demonstrating Z specifications. We describe how Z specifications may be animated using Crystal, but go on to present a prototype CASE tool, known as Zappa, that may be used to create and demonstrate faithful animations of Z specifications. The thesis starts with a thorough review of software engineering and of the development and rise of formal methods. The development of the OPERATOR approach is then given along with a review of animation, a description of the Crystal technique, and the development of the CASE tool Zappa. An evaluation of the research against the stated aims is presented and areas where future research is needed are pointed out.