Browse by author
Lookup NU author(s): Dr Zoe Andrews, Dr Jeremy Bryans, Professor John Fitzgerald, John Hughes, Dr Richard Payne, Dr Ken Pierce, Dr Stephen RiddleORCiD
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.
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
