Retrenchment Tutorial

The various theories of model based refinement that have arisen over the years offer powerful methods of transforming abstract formal models into (what are ultimately) implementations, with a high degree of assurance that suitable properties of the abstract model have been preserved. Formal model based refinement has had considerable success in selected critical projects such as the Meteor Project for the Paris Metro and a number of smartcard based developments such as the Mondex Purse and the Javacard. However, refinement is very demanding as regards the precise relationship between abstract models and their more concrete counterparts, and these aspects can inhibit its use, or at least undermine its connection to system requirements