Affiliations: School of Computer Science, University of Manchester,
Manchester M13 9PL, UK. E-mail: {banach,cj}@cs.man.ac.uk | School of Electronics and Computer Science, University
of Southampton, Southampton SO17 1BJ, UK. E-mail: [email protected] | Department of Computer Science, University of York,
York YO10 5DD, UK. E-mail: [email protected]
Abstract: 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 formal
development provides a highly credible testbed for examining how real world
refinement difficulties can be treated via retrenchment. The contributions of
retrenchment to integrating the real implementation with the formal development
are surveyed, and the extraction of commonly occurring 'retrenchment patterns'
is recalled. One of the Mondex difficulties, the 'Balance Enquiry Quandary' is
treated in detail, and the way that retrenchment is able to account for the
system behaviour is explained. The problem is reconsidered using generalised
forward refinement, and the simplicity of the resolution of the quandary, both
by retrenchment, and by generalised forward refinement, inspires the creation
of a genuine (1,1) forward refinement forMondex, something long thought
impossible. The forward treatment exhibits a similar balance enquiry quandary
to the backward refinement, as it must, given that both are refinements of an
atomic action to a non-atomic protocol, and the forward quandary is dealt with
as easily by retrenchment as is the backward case. The simplicity of the
retrenchment treatment foreshadows a general purpose retrenchment Atomicity
Pattern for dealing with atomic-versus-finegrained situations.
