Writing and animating Z specifications.

ANDREWS, Simon John. (1996). Writing and animating Z specifications. Doctoral, Sheffield Hallam University (United Kingdom)..

Preview

PDF (Version of Record) 10694158.pdf - Accepted Version All rights reserved. Download (9MB) | Preview

Abstract

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.

Item Type:	Thesis (Doctoral)
Additional Information:	Thesis (Ph.D.)--Sheffield Hallam University (United Kingdom), 1996.
Research Institute, Centre or Group - Does NOT include content added after October 2018:	Sheffield Hallam Doctoral Theses
Depositing User:	EPrints Services
Date Deposited:	10 Apr 2018 17:18
Last Modified:	26 Apr 2021 11:24
URI:	https://shura.shu.ac.uk/id/eprint/19278

Actions (login required)

View Item

Downloads

Publication Metrics