JUCS - Journal of Universal Computer Science 7(11): 952-979, doi: 10.3217/jucs-007-11-0952
Verification of ASM Refinements Using Generalized Forward Simulation
expand article infoGerhard Schellhorn
‡ University of Augsburg, Germany
Open Access
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.
refinement, forward simulation, data refinement, commuting diagrams, Abstract State Machines, transition systems, I/O-Automata, dynamic logic, correctness proofs, interactive theorem proving, compiler cerification