The bounded retransmission protocol must be on time!

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

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

    47 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 languageEnglish
    Title of host publicationTools and Algorithms for the Construction and Analysis of Systems
    Subtitle of host publicationThird International Workshop, TACAS'97, Enschede, The Netherlands, April 2-4, 1997, Proceedings
    EditorsEd Brinksma
    Place of PublicationBerlin
    PublisherSpringer
    Pages416-431
    Number of pages16
    ISBN (Electronic)978-3-540-68519-7
    ISBN (Print)978-3-540-62790-6
    DOIs
    Publication statusPublished - 1997
    Event3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1997 - University of Twente, Enschede, Netherlands
    Duration: 2 Apr 19974 Apr 1997
    Conference number: 3

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer
    Volume1217
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Workshop

    Workshop3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1997
    Abbreviated titleTACAS
    Country/TerritoryNetherlands
    CityEnschede
    Period2/04/974/04/97

    Keywords

    • FMT-MC: MODEL CHECKING
    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

    Fingerprint

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

    Cite this