The Bounded Retransmission Protocol must be on time!

P.R. d' Argenio, J.-P. Katoen, T.C. Ruys, G.J. Tretmans

    Research output: Book/ReportReportProfessional

    65 Citations (Scopus)
    80 Downloads (Pure)


    This paper concerns the transfer of files via a lossy communication channel. It formally specifies this file transfer service in a property-oriented way and investigates -using two different techniques -whether a given bounded retransmission protocol conforms to this service. This protocol is based on the well-known alternating bit protocol but allows for a bounded number of retransmissions of a chunk, i.e., part of a file, only. So, eventual delivery is not guaranteed and the protocol may abort the file transfer. We investigate to what extent real-time aspects are important to guarantee the protocol's correctness and use Spin and Uppaal model checking for our purpose.
    Original languageEnglish
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages63
    Publication statusPublished - 1997

    Publication series

    NameCTIT technical report
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)


    Dive into the research topics of 'The Bounded Retransmission Protocol must be on time!'. Together they form a unique fingerprint.
    • The bounded retransmission protocol must be on time!

      d' Argenio, P. R., Katoen, J-P., Ruys, T. C. & Tretmans, J., 1997, Tools and Algorithms for the Construction and Analysis of Systems: Third International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings. Brinksma, E. (ed.). Berlin: Springer, p. 416-431 16 p. (Lecture Notes in Computer Science; vol. 1217).

      Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

      Open Access
      35 Downloads (Pure)

    Cite this