Retrenchments, Refinements, and the Mondex Electronic Purse
- Speaker: Dr Richard Banach (University of Manchester)
- Host: Ian Pratt-Hartmann
- 11th October 2006 at 14:15 in 1.5
Some of the success stories of model based refinement are recalled, as well as some of the annoyances that arise when refinement is deployed in the engineering of large systems. The way that retrenchment attempts to alleviate such inconveniences is briefly reviewed. The Mondex Electronic Purse development provides a highly credible testbed for examining how real world refinement difficulties can be treated via retrenchment. The purse refinement provides four 'retrenchment opportunities', i.e. requirements issues that were handled in a less than ideal manner due to the restrictions of refinement, and the talk reviews work on all of them. Three of them (sequence number, log, hash) yield to a treatment via the retrenchment Tower Pattern. The fourth (balance enquiry) requires an examination of the entire purse protocol, and is treated via a retrenchment-enhanced refinement. The balance enquiry leads to alternative refinements for Mondex, namely a generalised forward refinement, and a (1,1) forward refinement. The latter settles a decade-old open problem for Mondex: whether the original (1,1) backward refinement was necessary, or whether a (1,1) forward refinement was in fact possible.