Portal de Periódicos da CAPES

Eternity variables to prove simulation of specifications

2005; Association for Computing Machinery; Volume: 6; Issue: 1 Linguagem: Inglês

10.1145/1042038.1042044

1557-945X

Wim H. Hesselink,

Simulation Techniques and Applications

Simulations of specifications are introduced as a unification and generalization of refinement mappings, history variables, forward simulations, prophecy variables, and backward simulations. A specification implements another specification if and only if there is a simulation from the first one to the second one that satisfies a certain condition. By adding stutterings, the formalism allows that the concrete behaviors take more (or possibly less) steps than the abstract ones.Eternity variables are introduced as a more powerful alternative for prophecy variables and backward simulations. This formalism is semantically complete: every simulation that preserves quiescence is a composition of a forward simulation, an extension with eternity variables, and a refinement mapping. This result does not need finite invisible nondeterminism and machine closure as in the Abadi--Lamport Theorem. The requirement of internal continuity is weakened to preservation of quiescence.Almost all concepts are illustrated by tiny examples or counter-examples.