ASM Refinement Preserving Invariants

12 years 9 months ago
ASM Refinement Preserving Invariants
: 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. Key Words: Refinement, Forward Simulation, Data Refinement, Commuting Diabstract State Machines, Mondex, El...
Gerhard Schellhorn
Added 13 Dec 2010
Updated 13 Dec 2010
Type Journal
Year 2008
Where JUCS
Authors Gerhard Schellhorn
Comments (0)