Methods and Tools for the Verification of Critical Properties

  • Roger Bishop Jones
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


This paper discusses methods for the formal treatment of critical systems.

The discussion is based on experience at ICL in the application of formal methods to the development of highly assured secure systems.

Problems arising in the use of the standard paradigm for specification and refinement in Z are identified and discussed. Alternative methods which overcome some of these difficulties are presented.

A fully worked example is provided showing how the prototype ICL Z proof support tool may be used to specify and verify the critical properties of a secure system.

The paper argues that effective use of formal methods in establishing, with high levels of assurance, that critical systems meet their critical requirements demands methods distinct from those typically advocated for general applications.


Formal Method Secure System Critical Property Critical System Critical Requirement 
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]
    R.D. Arthan. Formal Specification of a Proof Tool. In S.Prehn and W.J.Toetenel, editors, VDM ‘81, Formal Software Development Methods, LNCS 551, volume 551, pages 356–370. Springer-Verlag, 1991.Google Scholar
  2. [2]
    R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988.Google Scholar
  3. [3]
    Michael J.C. Gordon. HOL:A Proof Generating System for Higher-Order Logic. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer, 1987.Google Scholar
  4. [4]
    Michael J.C. Gordon, Arthur J. Milner, and Christopher P. Wadsworth. Edinburgh LCF. Lecture Notes in Computer Science. Vol. 78. Springer-Verlag, 1979.Google Scholar
  5. [5]
    Jeremy Jacob. On The Derivation of Secure Components. proc 1989 IEEE Symposium on Security and Privacy, pages 242–247, 1989.Google Scholar
  6. [6]
    R.Milner. A Theory of Type Polymorphism in Programming. Journal of Computer and System Sciences, 17: 348–375, 1978.MathSciNetCrossRefGoogle Scholar
  7. [7]
    J.M. Spivey. Understanding Z. Cambridge University Press, 1988.Google Scholar
  8. [8]
    J.M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1989.Google Scholar

Copyright information

© Springer-Verlag London 1992

Authors and Affiliations

  • Roger Bishop Jones
    • 1
  1. 1.International Computers LimitedWinnersh, BerksEngland

Personalised recommendations