Methods and Tools for the Verification of Critical Properties
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.
Unable to display preview. Download preview PDF.
- 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
- R.S. Boyer and J.S. Moore. A Computational Logic Handbook. Academic Press, 1988.Google Scholar
- 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
- 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
- Jeremy Jacob. On The Derivation of Secure Components. proc 1989 IEEE Symposium on Security and Privacy, pages 242–247, 1989.Google Scholar
- J.M. Spivey. Understanding Z. Cambridge University Press, 1988.Google Scholar
- J.M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, 1989.Google Scholar