Abstract
We have recently completed the specification and full refinement proof of a large, industrial scale application. The application was security critical, and the modelling and proof was done to increase the client’s assurance that the implemented system had no design flaws with security implications. Here we describe the application, and then discuss an essential lesson to learn concerning large proof contracts: that one must forge a path between mathematical formality on the one hand and practical achievement of results on the other. We present a number of examples of such decision points, explaining the considerations that must be made in each case.
In the course of our refinement work, we discovered that the traditional Z data refinement proof obligations [8, section 5.6], were not sufficient to prove our refinement. In particular, these obligations assume the use of a ‘forward’ (or ‘downward’) simulation. Here we present a more widely applicable set of Z data refinement proof obligations that we developed for and used on our project. These obligations allow both ‘forward’ and ‘backward’ simulations, and also allow non-trivial initialisation, finalisation, and input/output refinement.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Cooper, D., Stepney, S., Woodcock, J.: Refinement: Theory and Practice (In preparation)
Flynn, M., Hoverd, T., Brazier, D.: Formaliser – An interactive support tool for Z. In: Nicholls, J.E. (ed.) Z User Workshop, Oxford 1989, Workshops in Computing, pp. 128–141. Springer, Heidelberg (1990)
Jifeng, H., Hoare, C.A.R., Sanders, J.W.: Data refinement refined (resumé). In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187–196. Springer, Heidelberg (1986)
Josephs, M.B.: Specifying reactive systems in Z. Technical Report TR-19-91, Programming Research Group, Oxford University Computing Laboratory, UK, 303 (1991)
King, D.J., Arthan, R.D.: Development of Pract ical Verification Tools. The ICL Systems Journal 11(1) (May 1996)
Meisels, I., Saaltink, M.: The Z/EVES Reference Manual, Technical Report TR-97-5493-03c. ORA, 267 Richmond Road, Suite 100, Ottawa, Ontario, K1Z 6X3, Canada (June 1997), http://www.ora.on.ca/z-eves/
Michael Spivey, J.: The fuzz Manual. Computer Science Consultancy, 2nd edn., UK (1992), ftp://ftp.comlab.ox.ac.uk/pub/Zforum/fuzz
Michael Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. Prentice Hall International Series in Computer Science (1992)
Stepney, S.: Formaliser Home Page, http://public.logica.com/~formaliser/
Strulo, B.: How firing conditions help inheritance. In: Bowen, J.P., Hinchey, M.G. (eds.) ZUM 1995. LNCS, vol. 967, pp. 264–275. Springer, Heidelberg (1995)
Toyn, I.: Formal reasoning in the Z notation using CADiZ. In: Merriam, N.A. (ed.) 2nd International Workshop on User Interface Design for Theorem Proving Systems, Department of Computer Science, University of York (July 1996), http://www.cs.york.ac.uk/~ian/cadiz/home.html
Woodcock, J., Davies, J.: Using Z: Specification, Refinement, and Proof. Prentice Hall International Series in Computer Science (1996)
Z Notation version 1.2. Committee Draft Standard: CD13568. ISO panel JTC1/SC22/WG19, BSI panel IST/5/-/19/2 (September 1995), http://www.comlab.ox.ac.uk/oucl/groups/zstandards/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stepney, S., Cooper, D., Woodcock, J. (1998). More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds) ZUM ’98: The Z Formal Specification Notation. ZUM 1998. Lecture Notes in Computer Science, vol 1493. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-49676-2_20
Download citation
DOI: https://doi.org/10.1007/978-3-540-49676-2_20
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65070-6
Online ISBN: 978-3-540-49676-2
eBook Packages: Springer Book Archive