Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
type: Item
instance of: scholarly article
title: Parallel composition of assumption-commitment specifications: A unifying approach for shared variable and distributed message passing concurrency
zbMATH Open document ID: 0837.68025
published in: Acta Informatica
publication date: 1995-11-16T00:00:00Z
review text: Several compositional methods for the development of systems use the assumption commitment paradigm, by which a system (a process or a network of concurrent processes) is required to satisfy the commitment whenever it operates in an environment that respects the assumption. Compositional methods propose rules for deducing the correctness of concurrent process \(P_1 |P_2\) with respect to its specification from the correctness of the components \(P_1\) and \(P_2\) with respect to their specifications. It appears that the parallel rules for assumption- commitment specifications of state-based and message-based processes look remarkably different. In order to relate them, in the first part of the paper, a semantic parallel rule is formulated which abstracts from the way of communication. In that semantic framework, we consider abstract computations as labeled sequences of elements, where both elements and labels are left unspecified. We denote by \({\mathcal M} (P)\) the set of computations of a process \(P\) but omit the definition of the modeling function \(\mathcal M\). Then, a process is said to be correct with respect to an assumption-commitment specification if all the computations of the process are contained in the set of sequences corresponding to the specification. This set is constructed out of the set of computations allowed by the safety assumptions, the set of computations allowed by the safety assumptions, the set of computations allowed by the safety commitments, and the set of computations allowed by the general (safety and/or liveness) commitments. The set of computations of \(P_1 |P_2\) is denoted by \({\mathcal M} (P_1) \otimes {\mathcal M} (P_2)\) where the merging operator \(\otimes\) is again left unspecified. This operator behaves as a parameter of the semantic rule. In the second part of the paper, this semantic rule is gradually transformed into specific (language-dependent) rules for assumption-commitment specifications of state-based and mes…
Mathematics Subject Classification ID: 68Q10
Mathematics Subject Classification ID: 68Q55
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 814142
zbMATH Keywords: state-based message-based processes
zbMATH Keywords: correctness
zbMATH Keywords: concurrent process
zbMATH Keywords: specification
zbMATH Keywords: assumption-commitment specifications
zbMATH Keywords: semantic parallel rule
zbMATH Keywords: safety assumptions
zbMATH Keywords: process language
zbMATH Keywords: syntactic parallel rules
author: Antonio Cau
author: Pierre Collette
MaRDI profile type: Publication
full work available at URL: s002360050039
OpenAlex ID: W1753084406
cites work: A logical view of composition
cites work: Q3725528
cites work: A Theory of Communicating Sequential Processes
cites work: Application of the composition principle to unity-like specifications
cites work: An explanatory presentation of composition rules for assumption- commitment specifications
cites work: Q3359774
cites work: Q3998266
cites work: Tentative steps toward a development method for interfering programs
cites work: Proofs of Networks of Processes
cites work: P-A logic - a compositional proof system for distributed programs
cites work: Q3700812
cites work: Q3709867
cites work: A generalization of Owicki-Gries's Hoare logic for a concurrent while language
cites work: Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm
cites work: Q3347278
cites work: Q3681905
cites work: Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
DOI: 10.1007/S002360050039
description: scientific article; zbMATH DE number 814142