"Hard" systems development: from refinement to retrenchment
Formal refinement is the classical Formal Method of Hoare, He, Morgan, Abrial, Back among others, for the construction of verifiably correct software systems. Refinement, in simple terms, is a way of adding structure (data) and algorithms (operations) to an abstract model, or specification, of system requirements. A number of refinement steps transform a specification into code for a specific platform.
The strong assumptions of refinement restrict its expressiveness in certain application areas. Examples include continuous or control systems (typically described by classical physics), systems with notions of unbounded data types, and systems with interacting or conflicting requirements. An early motivating example was radiation dosimetry: the need, using experimental data, to compute radiation exposure profiles for given patient radiotherapy treatment plans. The approximation of an intricate physical model of radiation absorption in the body, by a grid of fixed-precision values cannot be done by refinemnt.
Building on intuitions about the need to liberalise or weaken classical refinement theory, my Ph.D. proposed the concept of retrenchment. The vehicle for the thesis was the B Method of J.-R. Abrial. In July 2001 I completed my part-time Ph.D. with the Formal Methods Group of the Computer Science Department at the University of Manchester, supervised by Dr. Richard Banach. The title is "Formal methods for continuous systems: liberalising refinement in B".
Retrenchment has matured as a new formal method: 17 papers are in print and a further 9 are in available in preprint form: see my publications page. The work is developing in a number of directions, all of which need further research:
- Requirements engineering and methodology. It is becoming increasingly clear that these is significant overlap between the Requirements Engineering and Software Development processes: implementation constraints of language, platform and distribution constrain, change and add to requirements identified at an early project stage. This is well known to practitioners of formal refinement, although the methodological aspects remain to be defined and developed. The cycle of refinement, requirement evolution, refinement breakage and subsequent repair is analogous to the physical process of annealing. It needs further investigation. In particular the utility of retrenchment (which can model any "broken" refinement) needs to be examined in this context.
- The integration of retrenchment and refinement
- Composition/decomposition of retrenchment and refinement.. The scalability of refinement from small- to large-scale development is reasonably understood; the scalability of retrenchment, and its combination with refinement, is not.
- Simulation and behavioural properties. The simulation aspect of refinement (whereby it is possible to glue small atomic refinements into larger composite behavioural refinements) does not hold in general for retrenchment; research is needed to develop understanding of the preservation of behavioural properties in retrenchment.
- Application case studies are required to develop understanding of retrenchment and refinement in practise. In Software Engineering, the skilful integration of theory and practice is key; real case studies add to and inform theory in an essential way.
- Tool support is needed for retrenchment and in its combination with refinement.
For a full retrenchment bibliography see http://www.cs.man.ac.uk/retrenchment/
Research and project work is available for the mathematically inclined; have a look at some of the papers.
Updated 23/2/05