Toggle Main Menu Toggle Search

ePrints

Modelling and Refinement of the MONDEX Electronic Purse in VDM

Lookup NU author(s): Dr Zoe Andrews, Dr Jeremy Bryans, Professor John Fitzgerald, John Hughes, Dr Richard Payne, Dr Ken Pierce, Dr Stephen Riddle

Downloads


Abstract

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.


Publication metadata

Author(s): Andrews Z, Bryans J, Fitzgerald J, Hughes J, Payne R, Pierce K, Riddle S

Publication type: Report

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2011

Pages: 82

Print publication date: 01/12/2011

Source Publication Date: December 2011

Report Number: 1308

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne


Share