Formal Refinement in Z: an electronic commerce application

I will talk about an industrial scale specification and refinement proof that we have performed for a security critical Smartcard application development. This development exposed several interesting issues to do with the industrial scale of the project. In addition, we discovered that the traditional Z data refinement rules were not sufficient to prove the refinement, and so we have developed some new Z refinement rules, to allow backward simulation, finalisation, and i/o refinement.

LS Home page or Talks in 1998/99