The Formal Specification in Z of Defence Standard 00–56
We give a formal specification of the safety analysis elements of the Revised Defence Standard 00–56, which describes procedures for the development of safety-critical systems. The specification is written in the Z notation, and, as it is an unusual application of formal methods, we reflect on the positive aspects of the experience as well as the main difficulties.
KeywordsEurope Meric Ambi
Unable to display preview. Download preview PDF.
- 1.S.M. Brien & J.E. Nicholls. Z Base Standard. Oxford University Computing Laboratory, Technical Monograph PRG-107. November 1992.Google Scholar
- 2.P.H.B. Gardiner. “Defence Standard 00–56: Development and Support Project. Formal Specification of Procedural Elements.” Formal Systems (Europe) Ltd, 3 Alfred Street, Oxford OX1 4EH, UK. FSEL/SRC/RDSPRC/1 version 4. 1. May 1993.Google Scholar
- 3.B. Potter, J. Sinclair, & D. Till. An Introduction to Formal Specification Using Z. Prentice Hall International. 1990.Google Scholar
- 4.J.M. Spivey. The Z Notation: A Reference Manual. 2nd Ed. Prentice Hall International. 1993.Google Scholar
- 5.J.M. Spivey. The fuzz Manual. 2nd Ed. Computer Science Consultancy. 1993.Google Scholar
- 6.Safety and Reliability Consultants Ltd (SRC), 89 High Street, Alton, Hampshire GU34 1LG, UK Revised Def Stan 00–56. SRC/SD/7102/4/TM/4. DraftB/19. 1. 93.Google Scholar
- 7.Safety and Reliability Consultants Ltd (SRC), 89 High Street, Alton, Hampshire GU34 1LG, UK Safety Analysis Elements — Revised Def Stan 00–56. SRC/SD/7102/4/TN/3. DraftA/18. 12. 92.Google Scholar
- 8.J. Woodcock & M. Loomes. Software Engineering Mathematics. Pitman. 1988.Google Scholar