Specification-oriented semantics for communicating processes
type: Item
instance of: scholarly article
title: Specification-oriented semantics for communicating processes
zbMATH Open document ID: 0569.68019
DOI: 10.1007/BF00268075
published in: Acta Informatica
publication date: 1986-01-01T00:00:00Z
review text: A process P satisfies a specification S, abbreviated P sat S, if every observation we can make about the behaviour of P is allowed by S. We use this idea of process correctness as a starting point for developing a specific form of denotational semantics for processes, called here specification-oriented semantics. This approach serves as a uniform framework for generating and relating a series of increasingly sophisticated denotational models for Communicating Processes. These models differ in the underlying structure of their observations which influences both the number of representable language operators and the notion of correctness expressed by P sat S. Safety properties are treated by all models; the more sophisticated models also permit proofs of liveness properties. An important feature of the models is a special hiding operator which abstracts from internal process activity. This allows large processes to be composed hierarchically from networks of smaller ones in such a way that proofs of the whole are constructed from proofs of its components. We also show consistency of the denotational models w.r.t. a simple operational semantics based on transitions which make internal process activity explicit.
Mathematics Subject Classification ID: 68N25
Mathematics Subject Classification ID: 68Q60
zbMATH DE Number: 3909722
zbMATH Keywords: specification
zbMATH Keywords: denotational semantics
zbMATH Keywords: specification-oriented semantics
zbMATH Keywords: communicating processes
zbMATH Keywords: correctness
zbMATH Keywords: liveness properties
author: Ernst-Rüdiger Olderog
author: Tony Hoare
MaRDI profile type: Publication
cites work: A Proof System for Communicating Sequential Processes
cites work: Formal Justification of a Proof System for Communicating Sequential Processes
cites work: Q3899466
cites work: Linear time and branching time semantics for recursion with merge
cites work: Q3681902
cites work: Processes and the denotational semantics of concurrency
cites work: Algebra of communicating processes with abstraction
cites work: Readies and Failures in the Algebra of Communicating Processes
cites work: Q3664417
cites work: A Theory of Communicating Sequential Processes
cites work: Q3680258
cites work: Semantics of nondeterminism, concurrency, and communication
cites work: A linear-history semantics for languages for distributed programming
cites work: Initial Algebra Semantics and Continuous Algebras
cites work: Algebraic semantics
cites work: Predicative programming Part I
cites work: A more complete model of communicating processes
cites work: Acceptance trees
cites work: Algebraic laws for nondeterminism and concurrency
cites work: Communicating sequential processes
cites work: A calculus of total correctness for communicating processes
cites work: Q3777424
cites work: Formal verification of parallel programs
cites work: A proof technique for communicating sequential processes
cites work: A calculus of communicating systems
cites work: Q3929062
cites work: Calculi for synchrony and asynchrony
cites work: Q3666248
cites work: Testing equivalences for processes
cites work: Q3700806
cites work: Proving Liveness Properties of Concurrent Programs
cites work: Power domains
cites work: Q3969890
cites work: Q3681905
description: scientific article; zbMATH DE number 3909722