Paper Info
Title
Completeness of fair ASM refinement
Abstract
ASM refinements are verified using generalized forward simulations which allow us to refine m abstract operations to n concrete operations with arbitrary m and n. One main difference from data refinement is that ASM refinement considers infinite runs and termination. Since backward simulation does not preserve termination in general, the standard technique of adding history information to the concrete level is not applicable to get a completeness proof. The power set construction also adds infinite runs and is therefore not applicable either. This paper shows that a completeness proof is nevertheless possible by adding infinite prophecy information, effectively moving nondeterminism to the initial state. Adding such prophecy information can be done not only on the semantic level, but also by a simple syntactic transformation that removes the choose construct of ASMs. The completeness proof is also translated to a completeness proof for IO automata. Finally, the proof is extended to deal with supplementary predicates, that specify fairness and liveness assumptions, by transferring a related result of Wim Hesselink for refinements that use the Abadi-Lamport setting.
Year
DOI
Venue
2011
10.1016/j.scico.2009.10.004
Sci. Comput. Program.
Keywords
Field
DocType
abstract state machines,asm refinement,io automata,arbitrary m,fairness,fair asm refinement,completeness,concrete operation,abadi–lamport,refinement,infinite prophecy information,history information,completeness proof,concrete level,infinite run,data refinement,prophecy information,abstract state machine
Programming language,Computer science,Automaton,Abstract state machines,Theoretical computer science,Predicate (grammar),Power set,Completeness (statistics),Syntax,Liveness
Journal
Volume
Issue
ISSN
76
9
Science of Computer Programming
Citations 
PageRank 
References 
10
0.51
28
Authors
1
Name
Order
Citations
PageRank
Gerhard Schellhorn176956.43