Article

Free access

Proving safety and liveness of communicating processes with examples

Authors:

J. Misra,

K. M. Chandy,

Todd SmithAuthors Info & Claims

PODC '82: Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing

Pages 201 - 208

https://doi.org/10.1145/800220.806698

Published: 18 August 1982 Publication History

PDF eReader

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.

References

[1]

Apt, K.R., N. Francez and W.P. de Roever, "A Proof System for Communicating Sequential Processes," TOPLAS, Vol. 2, July 1980.

Digital Library

Google Scholar

[2]

Hailpern, B.T., "Verifying Concurrent Processes Using Temporal Logic," Ph.D Thesis, Computer Systems Lab, Stanford University, August 1980.

Digital Library

Google Scholar

[3]

Hailpern, B. and S. Owicki, "Modular Verification of Computer Communication Protocols," Research Report RC8726, IBM Watson Research Center, March 1981.

Google Scholar

[4]

Levin, G.M. and D. Gries, "A Proof System for Communicating Sequential Processes," Acta Informatica 15, Springer-Verlag, 1981.

Google Scholar

[5]

Misra, J. and K.M. Chandy, "Proofs of Networks of Processes," IEEE-TSE, Vol. SE-7, No. 4, July 1981.

Google Scholar

[6]

Ossefort, M., "A Unified Approach to Formal Verification of Network Safety Properties," Ph.D thesis, Computer Sciences Department, University of Texas, 1982.

Digital Library

Google Scholar

[7]

Owicki, S. and L. Lamport, "Proving Liveness Properties of Concurrent Programs," Computer Systems Laboratory, Stanford University, 1980.

Google Scholar

Cited By

View all

Guerra HCosta J(2013)Processes with infinite liveness requirementsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2013.03.00182:3-4(137-161)Online publication date: Apr-2013
https://doi.org/10.1016/j.jlap.2013.03.001
Guerra HCosta J(2009)Processes with local and global liveness requirementsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2008.08.00378:3(117-137)Online publication date: Feb-2009
https://doi.org/10.1016/j.jlap.2008.08.003
Tanabe KSuzuki A(2007)Space‐time theory GQOT and its application to concurrent processesSystems and Computers in Japan10.1002/scj.469019110119:11(1-12)Online publication date: 21-Mar-2007
https://doi.org/10.1002/scj.4690191101
Show More Cited By

Recommendations

Proving Liveness and Termination of Systolic Arrays Using Communicating Finite State Machines

We model a systolic array as a network of, mostly identical, communicating finite state machines that exchange messages over one-to-one, unbounded, FIFO channels. Each machine has a cyclic behavior; in each cycle, a machine first receives one message ...
Beyond safety: customized SAT-based model checking
DAC '05: Proceedings of the 42nd annual Design Automation Conference

Model checking of safety properties has taken a significant lead over non-safety properties in recent years. To bridge the gap, we propose dedicated SAT-based model checking algorithms for properties beyond safety. Previous bounded model checking (BMC) ...
Relative liveness: from intuition to automated verification
ASYNC '95: Proceedings of the 2nd Working Conference on Asynchronous Design Methodologies

We point out deficiencies of previous treatments of liveness. We define a new liveness condition in two forms: one based on finite trace theory and the other on automata. We prove the equivalence of these two forms. We introduce a safety condition and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

PODC '82: Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing

August 1982

261 pages

ISBN:0897910818

DOI:10.1145/800220

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 August 1982

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Acceptance Rates

Overall Acceptance Rate 740 of 2,477 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
449
Total Downloads

Downloads (Last 12 months)32
Downloads (Last 6 weeks)2

Reflects downloads up to 14 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Guerra HCosta J(2013)Processes with infinite liveness requirementsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2013.03.00182:3-4(137-161)Online publication date: Apr-2013
https://doi.org/10.1016/j.jlap.2013.03.001
Guerra HCosta J(2009)Processes with local and global liveness requirementsThe Journal of Logic and Algebraic Programming10.1016/j.jlap.2008.08.00378:3(117-137)Online publication date: Feb-2009
https://doi.org/10.1016/j.jlap.2008.08.003
Tanabe KSuzuki A(2007)Space‐time theory GQOT and its application to concurrent processesSystems and Computers in Japan10.1002/scj.469019110119:11(1-12)Online publication date: 21-Mar-2007
https://doi.org/10.1002/scj.4690191101
Compton M(2005)Stenning's protocol implemented in UDP and verified in IsabelleProceedings of the 2005 Australasian symposium on Theory of computing - Volume 4110.5555/1082260.1082263(21-30)Online publication date: 1-Jan-2005
https://dl.acm.org/doi/10.5555/1082260.1082263
Stark E(2005)A proof technique for rely/guarantee propertiesFoundations of Software Technology and Theoretical Computer Science10.1007/3-540-16042-6_21(369-391)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-16042-6_21
Strom RYemini S(2005)The NIL distributed systems programming language: A status reportSeminar on Concurrency10.1007/3-540-15670-4_25(512-523)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-15670-4_25
Barringer HKuiper R(2005)Hierarchical development of concurrent systems in a temporal logic frameworkSeminar on Concurrency10.1007/3-540-15670-4_2(35-61)Online publication date: 29-May-2005
https://doi.org/10.1007/3-540-15670-4_2
Barringer H(2005)Misra & Chandy: Proofs of process networksA Survey of Verification Techniques for Parallel Programs10.1007/3-540-15239-3_20(84-98)Online publication date: 1-Jun-2005
https://doi.org/10.1007/3-540-15239-3_20
de Roever W(1999)The Need for Compositional Proof Systems: A SurveyCompositionality: The Significant Difference10.1007/3-540-49213-5_1(1-22)Online publication date: 21-May-1999
https://doi.org/10.1007/3-540-49213-5_1
Costa JSernadas A(1995)Progress assumption in concurrent systemsFormal Aspects of Computing10.1007/BF012146217:1(18-36)Online publication date: 1-Jan-1995
https://dl.acm.org/doi/10.1007/BF01214621
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Proving Liveness and Termination of Systolic Arrays Using Communicating Finite State Machines

Beyond safety: customized SAT-based model checking

Relative liveness: from intuition to automated verification