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. https://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: https://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: |
| ||||||
| 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: |
| ||||||
| 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 | ||||||
| DOI: | 10.1145/800220.806698 | ||||||
| Record Number: | CaltechAUTHORS:20190111-143826562 | ||||||
| Persistent URL: | https://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: | 16 Nov 2021 03:48 |
Repository Staff Only: item control page
