Verification of ASM Refinements Using Generalized Forward Simulation
Gerhard Schellhorn · Zenodo (CERN European Organization for Nuclear Research) · 2020
Abstract: This paper describes a generic proof method for the correctness of refine-ments of Abstract State Machines based on commuting diagrams. The method gener-alizes 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.