Skip to main content
SpringerLink
Log in

A Correctness Proof of the Bakery Protocol in μCRL

  • Conference paper
Algebra of Communicating Processes

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

A specification of a bakery protocol is given in μCRL. We provide a simple correctness criterion for the protocol. Then the protocol is proven correct using a proof system that has been developed for μCRL. The proof primarily consists of algebraic manipulations based on specifications of abstract data types and elementary rules and axioms from process algebra.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors. Proceedings of the International Workshop on Semantics of Specification Languages. Workshops in Computing, Springer-Verlag, 1994.

    Google Scholar 

  2. K.R. Apt. Ten years of Hoare’s logic, a survey, part I. ACM Transactions on Programming Languages and Systems, 3(4):431–483, 1981.

    Article  MATH  Google Scholar 

  3. K.R. Apt. Ten years of Hoare’s logic, a survey, part II: Nondeterminism. Theoretical Computer Science, 28:83–109, 1984.

    Article  MathSciNet  MATH  Google Scholar 

  4. J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

    Book  Google Scholar 

  5. M.A. Bezem and J.F. Groote. A correctness proof of a one bit sliding window protocol in μCRL. Technical Report 99, Logic Group Preprint Series, Utrecht University, 1993. To appear in the Computer Journal, Volume 37(4), 1994.

    Google Scholar 

  6. M.A. Bezem and J.F. Groote. A formal verification of the alternating bit protocol in the calculus of constructions. Technical Report 88, Logic Group Preprint Series, Utrecht University, March 1993.

    Google Scholar 

  7. K.M. Chandy and J. Misra. Parallel Program Design. A Foundation. Addison-Wesley, 1988.

    MATH  Google Scholar 

  8. H. Ehrig and B. Mahr. Fundamentals of algebraic specifications J, volume 6 of EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.

    Google Scholar 

  9. J.F. Groote and H. Korver. A correctness proof of the bakery protocol in μΟRL. Logic Group Preprint Series 80, Dept. of Philosophy, Utrecht University, October 1992.

    Google Scholar 

  10. J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. A case study in computer checked verification. Technical Report 100, Logic Group Preprint Series, Utrecht University, 1993.

    Google Scholar 

  11. J.F. Groote and A. Ponse. Proof theory for μCRL: a language for processes with data. In D.J. Andrews, e.a. [AGM94], pages 232–251. Full version is available as CWI Report CS-R9138, Amsterdam, The Netherlands, August 1991.

    Google Scholar 

  12. J.F. Groote and A. Ponse. The syntax and semantics of μCRL. In this volume: A. Ponse, C Verhoef and S.F.M. van Vlijmen, editors. Proceedings of ACP94. Workshops in Computing, Springer-Verlag, 1994.

    Google Scholar 

  13. R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics (extended abstract). In G.X. Ritter, editor, Information Processing 89, pages 613–618. North-Holland, 1989. Full version available as Report CS-R9120, CWI, Amsterdam, 1991.

    Google Scholar 

  14. H. Korver. Protocol Verification in μCRL PhD thesis, University of Amsterdam, 1994.

    Google Scholar 

  15. H. Korver and J. Springintveld. A computer-checked verification of Milner’s scheduler. In M. Hagiya and J.C. Mitchel, editors. Proceedings of the 2 nd International Symposium on Theoretical Aspects of Computer Software, TACS ’94, Sendai, Japan, pages 161–178, volume 789 of Lecture Notes in Computer Science. Springer-Verlag, 1994.

    Google Scholar 

  16. R. Milner. Communication and Concurrency. Prentice-Hall International, Englewood Cliffs, 1989.

    MATH  Google Scholar 

  17. M.P.A. Sellink. Verifying process algebra proofs in type theory. In Andrews et al. [AGM94], pages 315–339.

    Google Scholar 

  18. A.S. Troelstra and D. van Dalen. Constructivism in Mathematics, An Introduction (vol I). North-Holland, 1988.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS, Utrecht, The Netherlands

    Jan Friso Groote

  2. Department of Software Technology, CWI, Kruislaan 413, 1098 SJ, Amsterdam, The Netherlands

    Henri Korver

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Henri Korver
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Programming Research Group, University of Amsterdam, Kruislaan 403, 1098 SJ, Amsterdam, The Netherlands

    A. Ponse PhD

  2. Department of Mathematics and Computing Science, Eindhoven University of Technology, PO Box 513, 5600 MB, Eindhoven, The Netherlands

    C. Verhoef PhD

  3. Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS, Utrecht, The Netherlands

    S. F. M. van Vlijmen Drs.

Rights and permissions

Reprints and permissions

Copyright information

© 1995 British Computer Society

About this paper

Cite this paper

Groote, J.F., Korver, H. (1995). A Correctness Proof of the Bakery Protocol in μCRL. In: Ponse, A., Verhoef, C., van Vlijmen, S.F.M. (eds) Algebra of Communicating Processes. Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-2120-6_3

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-2120-6_3

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19909-0

  • Online ISBN: 978-1-4471-2120-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation