Verification of ASM Refinements Using Generalized Forward Simulation

Abstract

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.