Mondex ASM Refinement

This Web presentation shows a formalisation of the Mondex case study using ASM refinement. The emphasis here is on the systematic development of the simulation relation and the necessary invariant (the latter corresponding to the second refinement of the original case study given in [mondex00]). A description of the results of this case study can be found in [Mondex-ASM07] and this technical report . The presentation is divided into two layers (called projects in KIV) of specifications and theorems:
[Mondex00] S. Stepney and D. Cooper and J, Woodcock, AN ELECTRONIC PURSE Specification, Refinement and Proof, Technical Monograph, Oxford University Computing Laboratory, PRG-126 available here
[Mondex-ASM07] Gerhard Schellhorn and Holger Grandy and Dominik Haneberg and Nina Moebius and Wolfgang Reif, A Systematic Verification Approach for Mondex Electronic Purses using ASMs, Proceedings of the Dagstuhl Seminar on Rigorous Methods for Software Construction and Analysis,Springer,2007, submitted
[Boe03] E. Börger, The ASM Refinement Method, Formal Aspects of Computing, 2003
[SchJUCS01] G. Schellhorn, Verification of ASM Refinements Using Generalized Forward Simulation, Journal of Universal Computer Science, Vol. 7(11),pp. 952--979,2001, available here
[Sch05] G. Schellhorn, ASM Refinement and Generalizations of Forward Simulation in Data Refinement: A Comparison,Journal of Theoretical Computer Science, vol. 336, no. 2-3, pp. 403-435 ,2005