Skip to main content
SpringerLink
Log in

A proof system for asynchronously communicating deterministic processes

  • Contributions
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1994 (MFCS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 841))

Abstract

We introduce communication and synchronization constructs which allow deterministic processes, which communicate asynchronously via unbounded FIFO buffers, to cope with an indeterminate environment. We develop for the resulting parallel programming language, which subsumes deterministic dataflow, a simple compositional proof system. Reasoning about communication and synchronization is formalized in terms of input/output variables which record for each buffer the sequence of values sent and received. These input/output variables provide an abstraction of the usual notion of history variables which denote sequences of communication events. History variables are in general necessary for compositional reasoning about the correctness of distributed systems composed of non-deterministic processes.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K.R. Apt, N. Francez, and W.P. de Roever. A proof system for communicating sequential processes. ACM-TOPLAS, 2(3):359–385, 1980.

    Google Scholar 

  2. N. Francez. Program Verification. Addison Wesley, 1992.

    Google Scholar 

  3. 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, number 24 in LNCS, pages 343–395, 1986.

    Google Scholar 

  4. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6:319–340, 1976.

    Google Scholar 

  5. P.K. Pandya. Compositional Verification of Distributed Programs. PhD thesis, Tata Institute of Fundamental Research, Homi Bhabha Road, Bombay 400 005, INDIA, 1988.

    Google Scholar 

  6. J.V. Tucker and J.I. Zucker. Program Correctness over Abstract Data Types, with Error-State Semantics. CWI Monographs 6. North-Holland, 1988.

    Google Scholar 

  7. 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, number 194 in LNCS, 1985.

    Google Scholar 

  8. J. Zwiers. Compositionality, Concurrency and Partial Correctness. PhD thesis, Technical University Eindhoven, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Math. and Comp. Sc., Free University of Amsterdam, De Boelelaan 1081a, 1081, HV Amsterdam, The Netherlands

    F. S. de Boer

  2. Dept. of Comp. Sc., Utrecht University, P.O. Box 80089, 3508, TB Utrecht, The Netherlands

    M. van Hulst

Authors
  1. F. S. de Boer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. M. van Hulst
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Igor Prívara Branislav Rovan Peter Ruzička

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

de Boer, F.S., van Hulst, M. (1994). A proof system for asynchronously communicating deterministic processes. In: Prívara, I., Rovan, B., Ruzička, P. (eds) Mathematical Foundations of Computer Science 1994. MFCS 1994. Lecture Notes in Computer Science, vol 841. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58338-6_72

Download citation

  • DOI: https://doi.org/10.1007/3-540-58338-6_72

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58338-7

  • Online ISBN: 978-3-540-48663-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation