The Formal Specification in Z of Defence Standard 00–56

  • J. C. P. Woodcock
  • P. H. B. Gardiner
  • J. R. Hulance
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


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.


Formal Method Risk Class Formal Text None None Probability Target 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    S.M. Brien & J.E. Nicholls. Z Base Standard. Oxford University Computing Laboratory, Technical Monograph PRG-107. November 1992.Google Scholar
  2. 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. 3.
    B. Potter, J. Sinclair, & D. Till. An Introduction to Formal Specification Using Z. Prentice Hall International. 1990.Google Scholar
  4. 4.
    J.M. Spivey. The Z Notation: A Reference Manual. 2nd Ed. Prentice Hall International. 1993.Google Scholar
  5. 5.
    J.M. Spivey. The fuzz Manual. 2nd Ed. Computer Science Consultancy. 1993.Google Scholar
  6. 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. 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. 8.
    J. Woodcock & M. Loomes. Software Engineering Mathematics. Pitman. 1988.Google Scholar

Copyright information

© Formal Systems (Europe) Ltd 1994

Authors and Affiliations

  • J. C. P. Woodcock
    • 1
    • 2
  • P. H. B. Gardiner
    • 1
    • 2
  • J. R. Hulance
    • 3
  1. 1.Formal Systems (Europe) LtdOxfordUK
  2. 2.Programming Research GroupOxford University Computing LaboratoryOxfordUK
  3. 3.Formal Systems (Europe) LtdUK

Personalised recommendations