Abstract
In this paper we present a simple compositional Hoare logic for reasoning about the correctness of a certain class of distributed systems. We consider distributed systems composed of processes which interact asynchronously via unbounded FIFO buffers. The simplicity of the proof system is due to the restriction to local nondeterminism in the description of the sequential processes of a system. To illustrate the usefulness of the proof system we use PVS (Prototype Verification System, see [ORS92]) to prove in a compositional manner the correctness of a heartbeat algorithm for computing the topology of a network.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
K.R. Apt, N. Francez, and W.-P. de Roever. A proof system for communicating sequential processes. ACM-TOPLAS, 2(3):359–385, 1980.
Gregory R. Andrews. Concurrent Programming, Principles and Practice. The Benjamin/Cummings Publishing Company, Inc., 1991.
D. A. Cyrluk and M. K. Srivas. Theorem proving: Not an esoteric diversion, but the unifying framework for industrial verification. In IEEE International Conference on Computer Design (ICCD) '95, Austin, Texas, October 1995.
F.S. de Boer. Compositionality and completeness of the inductive assertion method for concurrent systems. In Proc. IFIP Working Conference on Programming Concepts, Methods and Calculi, San Miniato, Italy, 1994.
F.S. de Boer, J. Hooman, and W.-P. de Roever. State-based proof theory of concurrency: from noncompositional to compositional methods. Draft of a book.
F.S. de Boer and M. van Hulst. A proof system for asynchronously communicating deterministic processes. In B. Rovan I. Prívara and P. Ružička, editors, Proc. MFCS '94, volume 841 of Lecture Notes in Computer Science, pages 256–265. Springer-Verlag, 1994.
F.S. de Boer and M. van Hulst. A compositional proof system for asynchronously communicating processes. In Proceedings MPC'95, Kloster Irsee, Germany, 1995.
F.S. de Boer and M. van Hulst. Local nondeterminism in asynchronously communicating processes. Technical report, Utrecht University, 1996. In Preparation.
N. Francez. Program Verification. Addison Wesley, 1992.
J. Hooman and W.-P. de Roever. The quest goes on: a survey of proof systems for partial correctness of CSP. In Current trends in concurrency, volume 224 of Lecture Notes in Computer Science, pages 343–395. Springer-Verlag, 1986.
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Ada Informatica, 6:319–340, 1976.
S. Owre, J. Rushby, and N. Shankar. PVS: A prototype verification system. In 11th Conference on Automated Deduction, volume 607 of Lecture Notes in Artificial Intelligence, pages 748–752. Springer-Verlag, 1992.
P.K. Pandya. Compositional Verification of Distributed Programs. PhD thesis, Tata Institute of Fundamental Research, Homi Bhabha Road, Bombay 400 005, INDIA, 1988.
S. Rajan. Transformations in high-level synthesis: Formal specification and efficient mechanical verification. Technical Report CSL-94–10, CSL, 1994.
J. Zwiers, W.-P. de Roever, and P. van Emde Boas. Compositionality and concurrent networks: Soundness and completeness of a proofsystem. In Proc. ICALP'85, volume 194 of Lecture Notes in Computer Science. Springer-Verlag, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1996 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Boer, F.S., van Hulst, M. (1996). Local nondeterminism in asynchronously communicating processes. In: Gaudel, MC., Woodcock, J. (eds) FME'96: Industrial Benefit and Advances in Formal Methods. FME 1996. Lecture Notes in Computer Science, vol 1051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60973-3_97
Download citation
DOI: https://doi.org/10.1007/3-540-60973-3_97
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60973-5
Online ISBN: 978-3-540-49749-3
eBook Packages: Springer Book Archive