A model and temporal proof system for networks of processes
type: Item
instance of: scholarly article
title: A model and temporal proof system for networks of processes
zbMATH Open document ID: 0598.68025
DOI: 10.1007/BF01843567
author: B. George
published in: Distributed Computing
publication date: 1986-01-01T00:00:00Z
review text: An approach is presented for modeling networks of processes that communicate exclusively through message passing. A process (or a network) is defined by its set of possible behaviors, where each behavior is an abstraction of an infinite execution sequence of the process. The resulting model is simple and modular and facilitates information hiding. It can describe both synchronous and asynchronous networks. It supports recursively-defined networks and can characterize liveness properties such as progress of inputs and outputs, termination, and deadlock. A sound and complete temporal proof system based on the model is presented. It is compositional - a specification of a network is formed naturally from specifications of its components.
Mathematics Subject Classification ID: 68N25
zbMATH DE Number: 3965427
zbMATH Keywords: message passing
zbMATH Keywords: infinite execution sequence
zbMATH Keywords: synchronous and asynchronous networks
zbMATH Keywords: liveness properties
zbMATH Keywords: termination
zbMATH Keywords: deadlock
MaRDI profile type: Publication
cites work: Ten Years of Hoare's Logic: A Survey—Part I
cites work: Q4138149
cites work: Q4054644
cites work: Q4138147
cites work: A proof technique for communicating sequential processes
cites work: Q3939208
cites work: A calculus of communicating systems
cites work: Proofs of Networks of Processes
cites work: Q4485885
cites work: The incompleteness of Misra and Chandy's proof systems
cites work: Q3745263
description: scientific article; zbMATH DE number 3965427