CaltechAUTHORS
  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. http://resolver.caltech.edu/CaltechAUTHORS:20190111-143826562

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

Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechAUTHORS:20190111-143826562

Abstract

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
https://doi.org/10.1145/800220.806698DOIArticle
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.
Funders:
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:http://resolver.caltech.edu/CaltechAUTHORS:20190111-143826562
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:92222
Collection:CaltechAUTHORS
Deposited By: Tony Diaz
Deposited On:12 Jan 2019 17:03
Last Modified:12 Jan 2019 17:03

Repository Staff Only: item control page