Go home now Header Background Image
Submission Procedure
share: |
Follow us
Volume 7 / Issue 11

available in:   PDF (254 kB) PS (187 kB)
Similar Docs BibTeX   Write a comment
Links into Future
DOI:   10.3217/jucs-007-11-0952


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