Verification of ASM Refinements Using Generalized Forward Simulation

Gerhard Schellhorn (University of Augsburg, Germany)

Abstract: This paper describes a generic proof method for the correctness of refinements of Abstract State Machines based on commuting diagrams. The method generalizes forward simulations from the refinement of I/O automata by allowing arbitrary m:n diagrams, and by combining it with the refinement of data structures.

Keywords: Abstract State Machines, I/O-Automata, commuting diagrams, compiler cerification, correctness proofs, data refinement, dynamic logic, forward simulation, interactive theorem proving, refinement, transition systems

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