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.
Citation : Acta informatica, 33 (2), 1996, pp. 153-176
Research Group : Software Technology Research Laboratory (STRL)