Verification of ASM Refinements Using Generalized Forward Simulation
Дата
Авторы
Schellhorn,Gerhard
Journal Title
Journal ISSN
Volume Title
Издатель
Journal of Universal Computer Science
Аннотация
Описание
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