iBet uBet web content aggregator. Adding the entire web to your favor.
iBet uBet web content aggregator. Adding the entire web to your favor.



Link to original content: https://unpaywall.org/10.1007/BFB0014338
A bounded retransmission protocol for large data packets | SpringerLink
Skip to main content
Springer Nature Link
Log in

A bounded retransmission protocol for large data packets

A case study in computer checked algebraic verification

  • Conference
  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 1996)

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

  • 174 Accesses

Abstract

A protocol is described for the transmission of large data packets over unreliable channels. The protocol splits each data packet and broadcasts it in parts. In case of failure of transmission, only a limited number of retries is allowed (bounded retransmission), hence the protocol may give up the delivery of a part of the packet. Both the sending and the receiving client are informed adequately. This protocol is used in one of Philips' products.

We used μCRL as formal framework, a combination of process algebra and abstract data types. The protocol and its external behaviour are specified in μCRL. The correspondence between these is shown using the proof theory of μCRL. The whole proof of this correspondence has been computer checked using the proof checker Coq. This provides an example showing that proof checking of realistic protocols is feasible within the setting of process algebras.

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. J.C.M. Baeten and W.P. Weijland. Process Algebra. Cambridge Tracts in Theoretical Computer Science 18. Cambridge University Press, 1990.

    Google Scholar 

  2. M. Bezem, R. Bol, and J.F. Groote. Formalizing process algebraic verifications in the calculus of constructions. Technical Report 95-02, Eindhoven University of Technology, January 1995. To appear in Formal Aspects of Computing.

    Google Scholar 

  3. M.A. Bezem and J.F. Groote. A correctness proof of a one-bit sliding window protocol in μCRL The Computer Journal, 37(4):289–307, 1994.

    Google Scholar 

  4. G. Dowek, A. Felty, H. Herbelin, G. Huet, C. Murthy, C. Parent, C. Paulin-Mohring, and B. Werner. The Coq proof assistant user's guide. Version 5.8. Technical report, INRIA-Rocquencourt, May 1993.

    Google Scholar 

  5. J.F. Groote and H.P. Korver. A correctness proof of the bakery protocol in μCRL. In A. Ponse, C. Verhoef, and S.F.M. van Vlijmen, editors, Proc. 1st Workshop on the Algebra of Communicating Processes (ACP'94), Utrecht, Workshops in Computing, pages 63–86. Springer-Verlag, 1994.

    Google Scholar 

  6. J.F. Groote and A. Ponse. The syntax and semantics of μCRL. Technical Report CS-R9076, CWI, Amsterdam, December 1990.

    Google Scholar 

  7. J.F. Groote and A. Ponse. Proof theory for μCRL: a language for processes with data. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors, Proc. of the Int. Workshop on Semantics of Specification Languages, pages 232–251. Workshops in Computing, Springer Verlag, 1994.

    Google Scholar 

  8. J.F. Groote and J.C. van de Pol. A bounded retransmission protocol for large data packets. Technical Report Logic Group Preprint Series No. 100, Utrecht University, Oct 1993.

    Google Scholar 

  9. K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. Obtainable via http://www.csl.sri.com/∼shankar/shankar.html, 1995.

    Google Scholar 

  10. L. Helmink, M.P.A. Sellink, and F.W. Vaandrager. Proof-checking a data link protocol. In H.P. Barendregt and T. Nipkow, editors, Proc. of the 1st International Workshop “Types for Proofs and Programs”, May 1993, volume 806 of LNCS, pages 127–165, Nijmegen, 1994.

    Google Scholar 

  11. ISO. Information processing systems — open systems interconnection — LOTOS — a formal description technique based on the temporal ordering of observational behaviour ISO IS 8807, 1989.

    Google Scholar 

  12. H. Korver and J. Springintveld. A computer-checked verification of Milner's scheduler. In M. Hagiya and J.C. Mitchell, editors, Proc. of the Int. Symp. on Theoretical Aspects of Computer Software, volume 789 of LNCS, pages 161–178, Sendai, Japan, April 1994. Springer Verlag.

    Google Scholar 

  13. S. Mauw. PSF—A Process Specification Formalism. PhD thesis, University of Amsterdam, December 1991.

    Google Scholar 

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

    Google Scholar 

  15. M.P.A. Sellink. Verifying process algebra proofs in type theory. In D.J. Andrews, J.F. Groote, and C.A. Middelburg, editors, Proc. of the Int. Workshop on Semantics of Specification Languages, Utrecht 1993, Workshops in Computing, pages 315–339. Springer-Verlag, 1994.

    Google Scholar 

  16. M.P.A. Sellink. Computer-Aided Verification of Protocols, The Type Theoretic Approach. Phd thesis, Utrecht University, February 1996.

    Google Scholar 

Download references

Author information

Author notes

  1. Jan Friso Groote

    Present address: CWI, Kruislaan 413, 1089, SJ Amsterdam, The Netherlands

Authors and Affiliations

  1. Dept. of Philosophy, Utrecht University, The Netherlands

    Jan Friso Groote & Jaco van de Pol

Authors
  1. Jan Friso Groote
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Jaco van de Pol
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jan Friso Groote .

Editor information

Martin Wirsing Maurice Nivat

Rights and permissions

Reprints and permissions

Copyright information

© 1996 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Groote, J.F., van de Pol, J. (1996). A bounded retransmission protocol for large data packets. In: Wirsing, M., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1996. Lecture Notes in Computer Science, vol 1101. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014338

Download citation

  • DOI: https://doi.org/10.1007/BFb0014338

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-68595-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation