- Project ASM-INV-Refinement contains a formalization
of a variant of ASM Refinement [SchJUCS01][Boe03][Sch05]). This variant
preserves invariants. The theory is developed in 3 steps:
- First a purely algebraic theory of refinement is developed: trace-EF-AF defines a theory of traces (runs) and temporal operators (EF,AF) for an interpreter consisting of initial states, final states and a step relation. Specification forward defines the proof obligations for generalized forward simulation and forward-is-refine shows that these imply refinement (a form of trace inclusion that preserves a relation IO for infinite runs).
- In the second step this algebraic theory is used as the semantics of ASM rules using an embedding: specification DLinterpreter gives the abstract shape of an ASM rule (+ initial and final states). Based on this definition a relation over states with bottom (for nontermination) is defined (the semantics of the ASM rule). Then the notions of traces, temporal operators and refinement are lifted to show that the proof obligations for generalized forward simulation (now for ASM rules) are instances of those semantically defined, and imply refinement, which is now also expressed without explicit reference to bottom.
- The proof obligations are rather complex. Stronger conditions based on loops (instead of temporal operators) are usually satisfied in case studies (such as Mondex or WAM), and we show that they imply the fully general ones of Step 2.

- Project Mondex-ASM contains the Mondex case study itself. Its main specifications
and theorems are the following:
- Specification of the abstract ASM containing the transactions. and specification of the concrete ASM containing the communication protocol. Both ASMs specification uses various data types to build up their states. Two types of sets are involved: finite Sets that are term-generated by an empty set and an insert operation, and (potentially) infinite Sets , which are specified to be isomorphic to boolean functions via a .
- The main proof obligation of the refinement: , (commutativity of a diagram for simulation relation ACINV) is proven in specification ASM-refine . The specification of ACINV, which is based on a systematic definition of a local simulation relation LACINV for an individual purse, is also given in this specification. Because of this definition, the proof can be localised to a lemma for each purse that uses LACINV . Getting LACINV right such that this lemma is provable is the creative (and hard) part of the development. Note that the proof of the lemma is rather large but (nearly) fully automatic.
- The proof of the local simulation relation could be fully automated, by defining an invariant CINV for the concrete ASM (first only syntactically) that was used as an additional precondition. Every time the proof got stuck we looked at which property CINV should imply to close the proof. The resulting 26 properties are collected and proved here .
- The invariant CINV of the concrete ASM is also
defined using a local invariant LOCALINV . The main idea behing the local invariant
is simply: Every purse has done some steps into the protocol starting from
some old state (correspoding to the four axioms):
- for state idle, it has done no steps and is still in the old state
- for state epr, it has done a STARTFROM
- for state epv, it has done STARTTO
- for state epa, it has done STARTFROM and REQ

- In specification the full proof obligations for ASM refinement are shown. They are derived as instances of the generic ASM refinement theory there.
- Finally, we proves security of the abstract level , and using invariance preservation we also prove security of the communication protocol .

[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 |