Rensink, Arend and Gorrieri, Roberto (1995) Vertical Bisimulation. [Report]
|Abstract:||We investigate criteria to relate specifications and implementations belonging to conceptually different abstraction levels, and propose vertical bisimulation as a candidate relation for this purpose. Vertical bisimulation is indexed by a function mapping abstract actions onto concrete processes, which lays down the basic connection between the levels. Vertical bisimulation is compatible with the standard interleaving semantics; in fact, if the refinement function is the identity, then vertical bisimulation collapses to the standard notion of rooted bisimulation. We prove that vertical bisimulation satisfies a number of congruence-like proof rules (notably a structural one for recursion) that offer a powerful, compositional proof technique to verify whether a certain process is an implementation for some specification. We give a number of small examples to demonstrate the advantages of this approach.
|Link to this item:||http://purl.utwente.nl/publications/66677|
|Export this item as:||BibTeX|
Daily downloads in the past month
Monthly downloads in the past 12 months
Repository Staff Only: item control page