JUCS - Journal of Universal Computer Science 14(12): 1929-1948, doi: 10.3217/jucs-014-12-1929
ASM Refinement Preserving Invariants
expand article infoGerhard Schellhorn
‡ University of Augsburg, Germany
Open Access
Abstract
This paper gives a definition of ASM refinement suitable for the verification that a protocol implements atomic transactions. We used this definition as the basis of the formal verification of the refinements of the Mondex case study with the interactive theorem prover KIV. The refinement definition we give differs from the one we gave in earlier work which preserves partial and total correctness assertions of ASM runs. The reason is that the main goal of the refinement of the Mondex protocol is to preserve a security invariant, while total correctness is not preserved. To preserve invariants, the definition of generalized forward simulation is limited to the use of "small" diagrams, which contain of a single protocol step. We show a technique that allows to use the natural "big" diagrams that consist of an atomic action being refined by a full protocol run.
Keywords
refinement, forward simulation, data refinement, commuting diagrams, Abstract State Machines, Mondex, electronic purses, security, dynamic logic, weakest preconditions, interactive theorem proving