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 [Spivey 1992, 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.

@inproceedings(SS-ZUM11,
  author = "Susan Stepney and David Cooper and Jim Woodcock",
  title = "More Powerful {Z} Data Refinement:
           pushing the state of the art in industrial refinement",
  pages = "284--307",
  crossref = "ZUM11"
)

@proceedings(ZUM11,
  title = "The Z Formal Specification Notation, 
           11th International Conference of Z Users, 
           Berlin, Germany, September 1998",
  booktitle = "The Z Formal Specification Notation, 
           11th International Conference of Z Users, 
           Berlin, Germany, September 1998",
  editor = "Jonathan P. Bowen and Andreas Fett and Michael G. Hinchey",
  series = "LNCS",
  volume = 1493,
  publisher = "Springer",
  year = 1998
)