The Retrenchment Homepage

Welcome to the retrenchment homepage. Maintained by Richard Banach.
Last updated 27.03.13.

Retrenchment was introduced to address some of the perceived limitations of formal, model based refinement, for situations in which refinement might be regarded as desirable in principle, but turned out to be unusable, or nearly unusable, in practice.

For an introduction to retrenchment, you are invited to look at the retrenchment reference tutorial below.

The Retrenchment Reference Tutorial

This reference tutorial covers the motivations for retrenchment, what retrenchment is, and the currently perceived main technical points of interest. It is called a reference tutorial since it does not shirk from citing a fair amount of the mathematical detail, and already contains far too much to be presented in half a day. The idea is that it gives a terse summary of the technical state of the retrenchment art at any given time. In this sense it is a dynamic entity, responding to the evolution of the subject, and the inclination of the author(s) to prepare more material.

Live performances of suitable extracts from the reference tutorial can be arranged with the authors according to the needs of any given occasion. For private performances in the comfort of your own workstation: ensure you can see pdf, click the link below, select full screen mode, position your fingers over the arrow keys, and enjoy the show. (If that's too melodramatic, there is a 4-up printable version, with all the overlays taken out, in ps and pdf, at the link alongside.)

Retrenchment: an overview ..................... 4-up printable: ps / pdf

Supplementing the reference tutorial is a slideshow on the application of retrenchment to the Mondex Electronic Purse, a real world application formally developed using Z refinement, but which nevertheless furnishes a number of excellent "retrenchment opportunities" according to its lead author. (These are issues that were not treated in an ideal manner in the development due to the exigencies of refinement, but which can be approached more honestly using retrenchment.) Printable 4-up ps and pdf alongside.

Retrenchment and Mondex ..................... 4-up printable: ps / pdf

(For an introduction to the Mondex development see Susan Stepney's Smartcard web page in general, and the slideshow The Mondex purse Z refinement in particular.)

Other Tutorial Material

A tutorial on retrenchment applied to fault tree generation.

Retrenchment Publications

It is not the intention to maintain a detailed bibliography here; rather, to give pointers to where more detailed information can be found.

Most publications on retrenchment so far are co-authored by Richard Banach and so appear on my 'Recent Publications' page located via Richard Banach's homepage.

While detailed comments on individual papers are inappropriate, it is worth pointing out the presence of a series of papers that attempt to give a 'from scratch' development of retrenchment, written with some of the wisdom of experience, and in a consistent style, for those wanting a presentation more technically thoroughgoing than the tutorial. They are all on my publications page, and the first few in the series are:

Engineering and Theoretical Underpinnings of Retrenchment.
R. Banach, M. Poppleton, C. Jeske, S. Stepney
Sci. Comp. Prog., 67, 301-329, (2007)
Preprint: .......... Retrench.Underpin.pdf
(This paper, started in about 1999, gives an overview of motivations for introducing retrenchment, surveys key issues, and overviews two case studies: on digital control redesign, and on the Mondex Purse. This final version dates from the end of 2005, essentially.)

Composition Mechanisms for Retrenchment.
R. Banach, C. Jeske, M. Poppleton
J. Log. Alg. Prog., 75, 209-229, (2008)
Preprint: .......... Retrench.Composition.pdf
(Various composition mechanisms (vertical, horizontal, dataflow, fusion, etc.) are examined from a uniform perspective, bringing out their similarities.)

Model Based Refinement and the Design of Retrenchments.
R. Banach
Preprint: .......... Retrench.Designs.pdf
(The ideas in the `Underpinnings' paper are instantiated as retrenchment designs for Z, B, Event-B, VDM, RAISE, I/O-Automata, TLA+.)

Retrenchment and Refinement Interworking: the Tower Theorems.
R. Banach, C. Jeske
Math. Struc. Comp. Sci. (to appear)
Preprint: .......... Retrench.Tower.pdf
(A considered reappraisal and simplification of the results first demonstrated in Jeske's thesis (below). The present theorems are much easier to mechanise.)

Stronger Compositions for Retrenchments.
R. Banach, C. Jeske
J. Log. Alg. Prog., 79, 215-232, (2010)
Preprint: .......... Retrench.Strong.Comp.pdf
Preprint including full proofs: .......... Retrench.Strong.Comp.FULL.pdf
(Formerly dealing with output retrenchments, defaults, stronger compositions, and also feature engineering, the scope has been cut down in this final version. Now it focuses on stronger notions of vertical composition. The "FULL" preprint includes an appendix containing proofs omitted from the journal version.)

Simple Feature Engineering via Neat Default Retrenchments.
R. Banach, C. Jeske
J. Log. Alg. Prog., 80, 453-480, (2011)
Preprint: .......... Retrench.Feature.pdf
(An expanded treatement of the feature engineering material previously included in the "Stronger Compositions" paper.)

Retrenchment and System Properties.
R. Banach
Preprint: .......... Retrench.Props.pdf
(System properties (characterised as sets of (sequences of) execution fragments) and their mappings via retrenchment's bespoke simulation notion, are examined from the semantic standpoint.)

In addition to the above, it is worth pointing out some papers in the literature that deal with the Mondex "retrenchment opportunities", surveyed in the tutorial above. The first is an overview, the rest deal with individual "opportunities".

The Mondex Purse: Requirements and Retrenchments.
R. Banach
Preprint: .......... Retrench.Mondex.OvView.pdf

Retrenching the Purse: The Balance Enquiry Quandary, and Generalised and (1,1) Forward Refinements.
R. Banach, C. Jeske, M. Poppleton, S. Stepney
Fund. Inf. 77, 29-69, (2007)
Preprint: .......... Retrench.Mondex.Bal.pdf

Retrenching the Purse: Finite Sequence Numbers, and the Tower Pattern.
R. Banach, M. Poppleton, C. Jeske, S. Stepney
Proc. FM-05, LNCS 3582, 382-398, (2005)
J. Fitzgerald, I. Hayes, A. Tarlecki (eds.),
Preprint: .......... Retrench.Mondex.Seq.pdf

Retrenching the Purse: Finite Exception Logs, and Validating the Small.
R. Banach, C. Jeske, M. Poppleton, S. Stepney
Proc. IEEE/NASA SEW30-06, 234-245, (2006),
M. Hinchey (ed.),
Preprint: .......... Retrench.Mondex.Log.pdf

Retrenching the Purse: Hashing Injective CLEAR Codes, and Security Properties.
R. Banach, C. Jeske, M. Poppleton, S. Stepney
Proc. IEEE ISOLA-06, 82-90 (2007),
T. Margaria, B. Steffen (eds.),
Preprint: .......... Retrench.Mondex.Hash.pdf

Coarse Grained Retrenchment and the Mondex Denial of Service Attacks.
R. Banach
Proc. IEEE TASE-09, 103-110, (2009),
W. Chin, S. Qin (eds.),
Preprint: .......... Retrench.Mondex.CG.DOS.pdf

Other work

Authors of other work on retrenchment are invited to send me suitable pointers for inclusion here via banach "at" cs "dot" man "dot" ac "dot" uk.

Mike Poppleton's Publications Page

Czeslaw Jeske's PhD Thesis, the machinery behind the Tower Pattern.

Simon Fraser's PhD Thesis, on the experimental Frog Toolkit.