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.
KeywordsFormal Method Risk Class Formal Text None None Probability Target
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