Modelling and Refinement of the MONDEX Electronics Purse in VDM

摘要

We present the modelling and refinement of the Mondex Electronic Purse 'challenge problem'. Our approach uses the well-established Vienna Development Method. Abstract and concrete models are presented, with a refinement step that addresses error detection and recovery in the implementation. We exercise the range of verification and validation techniques associated with VDM (animation, testing and proof.) The study suggests future developments in machine-assisted proof to support the development of VDM models and their associated refinements. We compare the models and proof developed in this way with the approaches taken in several other contemporary studies of the Mondex system.