Vertical Implementation
Rensink, Arend and Gorrieri, Roberto (2001) Vertical Implementation. Information and Computation, 170 (1). pp. 95133. ISSN 08905401

PDF
352kB 
Abstract:  We investigate criteria to relate specifications and implementations belonging to conceptually different levels of abstraction. For this purpose, we introduce the generic concept of a vertical implementation relation, which is a family of binary relations indexed by a refinement function that maps abstract actions onto concrete processes and thus determines the basic connection between the abstraction levels. If the refinement function is the identity, the vertical implementation relation collapses to a standard (horizontal) implementation relation. As desiderata for vertical implementation relations we formulate a number of congruencelike proof rules (notably a structural rule for recursion) that offer a powerful, compositional proof technique for vertical implementation. As a candidate vertical implementation relation we propose vertical bisimulation. Vertical bisimulation is compatible with the standard interleaving semantics of process algebra; in fact, the corresponding horizontal relation is rooted weak bisimulation. We prove that vertical bisimulation satisfies the proof rules for vertical implementation, thus establishing the consistency of the rules. Moreover, we define a corresponding notion of abstraction that strengthens the intuition behind vertical bisimulation and also provides a decision algorithm for finitestate systems. Finally, we give a number of small examples to demonstrate the advantages of vertical implementation in general and vertical bisimulation in particular.

Item Type:  Article 
Copyright:  © 2001 Elsevier 
Faculty:  Electrical Engineering, Mathematics and Computer Science (EEMCS) 
Research Group:  
Link to this item:  http://purl.utwente.nl/publications/66680 
Official URL:  http://dx.doi.org/10.1006/inco.2001.2967 
Export this item as:  BibTeX EndNote HTML Citation Reference Manager 
Repository Staff Only: item control page
Metis ID: 203559