ETAPS 2009

ETAPS 2009 Retrenchment Tutorial

Date/Time/Place: T.B.D.

Presenter: Richard Banach, University of Manchester

Retrenchment, a formal development technique structurally similar to but different from model based refinement, was introduced to address some of the perceived limitations of refinement, for situations in which refinement might be regarded as desirable in principle, but in which it turns out to be unusable, or nearly unusable, in practice.

This tutorial gives an overview of retrenchment, and illustrates it in the context of a real industrial scale case study: the kind of place where the use of retrenchment to fill in discrepancies between an idealised refinement-theoretic perspective and the grittiness of real world detail is most convincing.

The tutorial is in two parts. The first part motivates the use of retrenchment, and covers its key technical properties, especially composition and the interaction with refinement. The second part covers the Mondex Electronic Purse (a smartcard purse for securely containing real money and securely performing real monetary transactions). Mondex was a development done using industrial strength Z refinement. Although it was done using state of the art techniques, a number of requirements issues, legitimately the concern of the formal development (since they could impact on the security properties of the purse if mishandled), were nevertheless set beyond the scope of the formal development, or handled in an unnatural manner, because of the demanding nature of the refinement proof obligations. These issues provide excellent "retrenchment opportunities", since they allow retrenchment to fill in the relevant gaps, and provide a convincing context within which the retrenchments used can be validated.