Paper Info
Title
More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement
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.
Year
DOI
Venue
1998
10.1007/978-3-540-49676-2_20
ZUM
Keywords
Field
DocType
industrial refinement,powerful z data refinement,input output
Software engineering,Formality,Systems engineering,Computer science,Formal specification,Proof obligation,Reactive system,Software development,Formal verification
Conference
Volume
ISSN
ISBN
1493
0302-9743
3-540-65070-9
Citations 
PageRank 
References 
40
2.38
3
Authors
3
Name
Order
Citations
PageRank
Susan Stepney1813113.21
David Cooper212316.91
Jim Woodcock353477.08