Modelling and Refinement of the MONDEX Electronic Purse in VDM

  1. Lookup NU author(s)
  2. Dr Zoe Andrews
  3. Dr Jeremy Bryans
  4. Professor John Fitzgerald
  5. John Hughes
  6. Dr Richard Payne
  7. Dr Ken Pierce
  8. Dr Stephen Riddle
Author(s)Andrews Z, Bryans J, Fitzgerald J, Hughes J, Payne R, Pierce K, Riddle S
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Source Publication DateDecember 2011
Report Number1308
Full text is available for this publication:
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.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
ActionsLink to this publication