Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern

The Mondex Electronic Purse system [18] is an outstanding example of formal refinement techniques applied to a genuine industrial scale application, and notably, was the first verification to achieve ITSEC level E6 certification. A bstract model including security properties, and a formal concrete model of the system design were developed, and a formal refinement was hand-proved between them in Z. Despite this success, certain requirements issues were set beyond the scope of the formal development, or handled in an unnatural manner. Retrenchment is reviewed in a form suitable for integration with Z refinement, and is used to address one such issue in detail: the finiteness of the transaction sequence number in the purse funds transfer protocol. A retrenchment is constructed from the lowest level model of the purse system to a model in which sequence numbers are finite, using a suitable elaboration of the Z promotion [21] e. We overview the lifting of that retrenchment to the ab...

• Type: Conference
• Year: 2005
• Where: FM
• Authors: Richard Banach, Michael Poppleton, Czeslaw Jeske, Susan Stepney
• Keywords: FM 2005, Formal Developments, Formal Refinement, Sequence Number