Vertical implementation

We investigate criteria to relate specifications and implementations belong ing to conceptually different levels of abstraction. For this purpose. we i ntroduce the generic concept of a vertical implementation relation, which i s a family of binary relations indexed by a refinement function that maps a bstract actions onto concrete processes and thus determines the basic conne ction between the abstraction levels. If the refinement function is the ide ntity, the vertical implementation relation collapses to a standard (horizo ntal) implementation relation. As desiderata for vertical implementation re lations we formulate a number of congruence-like proof rules (notably a str uctural rule for recursion) that offer a powerful, compositional proof tech nique for vertical implementation, As a candidate vertical implementation r elation we propose vertical bisimulation. Vertical bisimulation is compatib le with the standard interleaving semantics of process algebra; in fact, th e corresponding horizontal relation is rooted weak bisimulation. We prove t hat vertical bisimulation satisfies the proof rules for vertical implementa tion, 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 finite-sta te systems. Finally, we give a number of small examples to demonstrate the advantages of vertical implementation in general and vertical bisimulation in particular. (C) 2001 Academic Press.