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 M´et´eor 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. Examples of such scenarios arise in large scale discrete applications, where low level details can clutter the structure of abstract models to an extent that inhibits their proper incorporation in the abstract model. Others arise in the modelling of continuous systems, in which the controllers to be built are nonetheless digital, and thus the transition from modelling in the continuous domain to modelling in the discrete domain has to be overcome. In practice, situations like these are usually dealt with by ad hoc means that depend on the example at hand. (Typical strategies range from: changing the abstract model to fit the exigencies of refinement, to making the ‘mathematical’ concrete model subtly inconsistent with the actual executable code, to simply neglecting certain low level details in all the mathematical development.)