Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 14 / Issue 12

available in:   PDF (138 kB) PS (129 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-014-12-1929


ASM Refinement Preserving Invariants

Gerhard Schellhorn (University of Augsburg, Germany)

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: Abstract State Machines, Mondex, commuting diagrams, data refinement, dynamic logic, electronic purses, forward simulation, interactive theorem proving, refinement, security, weakest preconditions

Categories: D.2.1, D.2.4, D.3.1, D.4.6, F.3.1, F.4.1