Parallel composition of assumption-commitment specifications: a unifying approach for shared variable and distributed message passing concurrency

We unify the parallel composition rule of assumption-commitment specifications for respectively state-based and message-based concurrent processes. Without providing language-dependent definitions, we first assume that the model of a process can be given as a set of 'sequences' (e.g., traces, state sequences). Then we assume the existence of a merging operator that captures the compositionality of that model. On this basis, we formulate a semantic parallel composition rule for assumption-commitment specifications wherein the merging operator behaves as a parameter. Then, by providing suitable language-specific definitions for the model of a process and the merging operator, we transform the semantic rule into syntactic ones, both for the state-based and message-based approaches to concurrency.Antonio Cau partially supported by ESPRIT Project 6021 (REACT). Pierre Collette supported by National Fund for Scientific Research (Belgium