A Hierarchy of System Descriptions via Atomic Linear Refinement

Article type: Research Article

Authors: Gorrieri, Roberto^{; *}

Affiliations: Dipartimento di Matematica – Università di Bologna Piazza di Porta S. Donato 5, 1-40127 Bologna, Italy

Note: [*] Research performed in part when the author was at the University of Pisa, and supported by Esprit Basic Research Action n. 3011 CEDISYS.

Abstract: The problem of relating system descriptions at different levels of abstraction is studied in the field of Process Description Languages, following the so-called interleaving approach. Since we believe that several different languages should be used profitably during the hierarchical specification process, we investigate the problem of implementing a calculus into another one. As a case study, we introduce a pair of languages which will be increasingly enriched. The basic languages are sequential and nondeterministic; their first enrichment is obtained by adding an operator for asynchrony; then also communication is added, and finally restriction is dealt with. For each pair, the latter language extends the former with atomicity, obtained by adding to the signature of the former an operator of strong prefixing that makes atomic the execution of a sequence of actions. The two languages are intended to be a specification and an implementation language, respectively. To directly relate them, a mapping, called atomic linear refinement, is introduced from actions of the former to atomic sequences (i.e. sequences of actions built with strong prefixing) of the latter. An atomic linear refinement can be homomorphically extended to become a mapping among process terms of the two languages and thus also among the states of their associated transition systems. A notion of implementation, based on a sort of bisimulation (parametric with respect to an atomic action refinement), relates processes of the two languages. Given a specification process p and an atomic action refinement ρ, the refined process ρ(p) is proved to be an implementation of p. Moreover, a complete proof system for strong and weak equivalence are presented for both languages (and thus also for the operator of strong prefixing) and proved consistent with respect to refinement: if p and ρ are congruent processes of the specification language, then ρ(p) and ρ(q) are congruent, too.

DOI: 10.3233/FI-1992-163-406

Journal: Fundamenta Informaticae, vol. 16, no. 3-4, pp. 289-336, 1992