THE University of York

Using PVS to Prove a Z Refinement: A Case Study

David W.J. Stringer-Calvert, Susan Stepney, Ian Wand

Presented at Formal Methods Europe '97, Graz, Austria.
Proceedings published by Springer-Verlag.

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[Ste93] 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 hand 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.

dvi (you also need the EPS file for an included figure) and postscript

BibTeX Entry

@inproceedings{z-in-pvs,
	TITLE = {Using {PVS} to Prove a {Z} Refinement: A Case Study},
	AUTHOR = {David W.J. Stringer-Calvert and Susan Stepney and Ian Wand},
        INSTITUTION = {Department of Computer Science, University of York},
	BOOKTITLE = {{FME} '97: Formal Methods: Their Industrial Application 
                     and Strengthened Foundations},
	EDITOR = {John Fitzgerald and Cliff B. Jones and Peter Lucas},
        ADDRESS = {Gr{\"a}z, Austria},
	PUBLISHER = {Springer-Verlag},
	SERIES = {Lecture Notes in Computer Science},
	NUMBER = {1313},
	MONTH = sep,
	YEAR = 1997,
	PAGES = {573--588}
}
Return to my publications page

Return to the Computer Science Laboratory home page