"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:

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