Abstract
The development of critical systems often places undue trust in the software tools used. This is especially true of compilers, which are a weak link between the source code produced and the object code which is executed. Stepney [23] advocates a method for the production of trusted compilers (i.e. those which are guaranteed to produce object code that is a correct refinement of the source code) by developing a proof of a small, but non trivial compiler by hand in the Z specification language. This approach is quick, but the type system of Z is too weak to ensure that partial functions are correctly applied.
Here, we present a re-working of that development using the PVS specification and verification system. We describe the problems involved in translating from the partial set theory of Z to the total, higher order logic of the PVS system and the strengths and weaknesses of this approach.
Logica UK Ltd carried out the original work on the compiler method for RSRE (now DRA Malvern), and is continuing the development for AWE plc. D.W.J. Stringer Calvert is funded by a CASE studentship from the Engineering and Physical Sciences Research Council and Siemens Plessey Systems.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Rosalind Barden, Susan Stepney, and David Cooper. Z in Practice. BCS Practitioners Series. Prentice Hall International, 1994.
Jonathan Bowen, C.A.R. Hoare, Michael R. Hansen, Anders R. Ravn, Hans Rischel, Ernst-Rüdiger Olderog, Michael Schenke, Martin Fränzle, Markus Müller-Olm, Jifeng He, and Zheng Jianping. Provably correct systems-FTRTFT'94 tutorial. In Proceedings of FTRTFT'94, number 863 in Lecture Notes in Computer Science. Springer-Verlag, September 1994.
Robert S. Boyer and J. Strother Moore. A Computational Logic Handbook. Academic Press, 1988.
Karl-Heinz Buth. Automated code generator verification based on algebraic laws. ProCoS Project Document Kiel KHB 5/1, September 1995.
W.J. Cullyer. Implementing safety critical systems: The VIPER microprocessor. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 1–25. Kluwer Academic Publishers, 1988.
Paul Curzon. A verified vista implementation final report. Technical Report 311, University of Cambridge Computer Laboratory, September 1993.
Axel Dold, F.W. von Henke, H. Pfeifer, and H. Rueß. Formal verification of transformations for peephole optimizations. 1997. These proceedings.
Mike Gordon. A proof generating system for higher-order logic. Technical Report 103, University of Cambridge Computer Laboratory, January 1987.
Stanford Verification Group. Stanford Pascal verifier user manual. Technical Report 11, Stanford Verification Group, 1979.
Joshua D. Guttman, John D. Ramsdell, and Vipin Swarup. The VLISP verified scheme system. LISP and Symbolic Computation, 8:33–110, 1995.
R.W.S. Hale. Program compilation. In Jonathan Bowen, editor, Towards Verified Systems, chapter 6. Elsevier Science Publishers Series on Real-Time Safety Critical Systems, Amsterdam, 1993.
Jeffrey J. Joyce. A verified compiler for a verified microprocessor. Technical Report 167, University of Cambridge Computer Laboratory, March 1989.
A.C. Leisenring. Mathematical Logic and Hilbert's ε-symbol. Gordon and Breach Science Publishers, New York, 1969.
J. Strother Moore. A mechanically verified language implementation. Technical Report 30, Computational Logic Inc., September 1988.
I. T. Nabney and S. Stepney. High integrity separate compilation. In preparation.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
H. Pfeifer, A. Dold, F. W. v. Henke, and H. Rueß. Mechanized Semantics of Simple Imperative Programming Constructs. Ulmer Informatik-Berichte 96-11, Universität Ulm, Fakultät für Informatik, 1996.
Wolfgang Polak. Compiler Specification and Verification. Number 124 in Lecture Notes in Computer Science. Springer-Verlag, 1981.
J.M. Rushby and D.W.J. Stringer-Calvert. A less elementary tutorial for the PVS specification and verification system. Technical Report CSL-95-10, Computer Science Laboratory, SRI International, August 1996.
Mark Saaltink. The Z/EVES system. In ZUM '97. The Z Formal Specification Notation; 10th International Conference of Z Users, number 1212 in Lecture Notes in Computer Science, pages 72–85, Reading, UK, April 1997. Springer-Verlag.
J. M. Spivey. The fuzz manual. Computing Science Consultancy, 2 Willow Close, Oxford, UK, 1988.
J.M. Spivey. The Z Notation: A Reference Manual. Prentice Hall International, 1989.
Susan Stepney. High Integrity Compilation: A Case Study. Prentice Hall International, 1993.
Deborah Weber-Wulff. Proven correct scanning. Procos internal report, August 1992.
William D. Young. A verified code generator for a subset of Gypsy. Technical Report 33, Computational Logic Inc., October 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Stringer-Calvert, D.W.J., Stepney, S., Wand, I. (1997). Using PVS to prove a Z refinement: A case study. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds) FME '97: Industrial Applications and Strengthened Foundations of Formal Methods. FME 1997. Lecture Notes in Computer Science, vol 1313. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63533-5_30
Download citation
DOI: https://doi.org/10.1007/3-540-63533-5_30
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63533-8
Online ISBN: 978-3-540-69593-6
eBook Packages: Springer Book Archive