A Caltech Library Service

Proving safety and liveness of communicating processes with examples

Misra, J. and Chandy, K. M. and Smith, Todd (1982) Proving safety and liveness of communicating processes with examples. In: Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing. Association for Computing Machinery , New York, NY, pp. 201-208. ISBN 0-89791-081-8.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


A method is proposed for reasoning about safety and liveness properties of message passing networks. The method is hierarchical and is based upon combining the specifications of component processes to obtain the specification of a network. The inference rules for safety properties use induction on the number of messages transmitted; liveness proofs use techniques similar to termination proofs in sequential programs. We illustrate the method with two examples: concatenations of buffers to construct larger buffers and a special case of Stenning protocol for message communication over noisy channels.

Item Type:Book Section
Related URLs:
URLURL TypeDescription
Additional Information:© 1982 ACM. This work was supported by the Air Force Office of Scientific Research under grant AFOSR 81-0205 and the University Research Institute at the University of Texas.
Funding AgencyGrant Number
Air Force Office of Scientific Research (AFOSR)81-0205
University of TexasUNSPECIFIED
Subject Keywords:communicating processes, message-passing systems, proofs of process networks, safety, liveness
Classification Code:CR-Categories: C.2.2, C.2.4, D.1.3, F.3.1, F.3.2
Record Number:CaltechAUTHORS:20190111-143826562
Persistent URL:
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:92222
Deposited By: Tony Diaz
Deposited On:12 Jan 2019 17:03
Last Modified:16 Nov 2021 03:48

Repository Staff Only: item control page