5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000

Towards a Mechanised Software Development Method

Formal methods (FM) consist of a set of techniques and tools that are based on mathematical modeling and formal logic and which are employed to specify and verify requirements and designs for computer systems - both hardware and software. Moreover, the growing criticality and complexity of software has led to increased interest in applying FM to software specification and design as well.

The paper will develop a more practical software development method by integrating the Refinement Calculus with Z, both developed at Oxford University, and develop a software development environment inwhich software can be formally specified and refined into program code with all the refinement steps proved correct by the tool. We present acase study of using a refinement tool prototype, ZRefiner to refine a Z specification to code. The three-tier structure of ZRefiner deals with different applications in different tiers and makes ZRefiner more exible and efficient. Finally, potential theoretical and practical problems of implementing such a mechanised tool are discussed.

Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.

ERCIM FMICS Home Page, GMD FOKUS Home Page

Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch