The bounded retransmission protocol must be on time!

Hendrik Brinksma (Editor), P.R. d' Argenio, Joost P. Katoen, T.C. Ruys, G.J. Tretmans

    Research output: Contribution to conferencePaper

    30 Downloads (Pure)

    Abstract

    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. Supported by the NWO/SION project 612-33-006.
    Original languageUndefined
    Pages416-431
    Number of pages16
    DOIs
    Publication statusPublished - 1997

    Keywords

    • FMT-MC: MODEL CHECKING
    • EWI-6470
    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
    • IR-63292

    Cite this