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

Corresponding author: Gerhard Schellhorn ( schellhorn@informatik.uni-augsburg.de )

© Gerhard Schellhorn.
This article is freely available under the J.UCS Open Content License.
Citation: Schellhorn G (2001) Verification of ASM Refinements Using Generalized Forward Simulation. JUCS - Journal of Universal Computer Science 7(11): 952-979. https://doi.org/10.3217/jucs-007-11-0952
Open Access
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
refinement, forward simulation, data refinement, commuting diagrams, Abstract State Machines, transition systems, I/O-Automata, dynamic logic, correctness proofs, interactive theorem proving, compiler cerification