The Bounded Retransmission Protocol must be on time!

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

    Research output: Book/ReportReportProfessional

    54 Citations (Scopus)
    76 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 languageUndefined
    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)


    • IR-18600
    • METIS-119121
    • EWI-6034

    Cite this