Assertional verification of a connection management protocol

András L. Oláh, Sonia M. Heemstra de Groot

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

    4 Downloads (Pure)

    Abstract

    This paper deals with the verification of a connection management protocol which uses timestamps and network-wide synchronized clocks for the reliable opening and closing of connections. We prove the correctness of the protocol over an unreliable, bounded-delay network for the cases when (i) timestamps are unbounded; (ii) timestamps are from a finite modulo-N space. We determine the minimal safe value of N as a function of real-time parameters such as maximum packet lifetime, clock skew and maximum connection duration.

    The protocol is modeled as a state-transition system and we argue about the properties of the system using an assertional technique based on temporal logic. Apart from handling safety and progress properties, this framework is also suitable to describe real-time aspects of the system.
    Original languageEnglish
    Title of host publicationFormal Description Techniques VIII (FORTE '95)
    Subtitle of host publicationProceedings of the IFIP TC6 Eighth International Conference on Formal Description Techniques, Montreal, Canada, October 1995
    EditorsGregor von Bochmann, Rachida Dssouli, Omar Rafiq
    Place of PublicationLondon
    PublisherSpringer
    Pages401-416
    ISBN (Electronic)978-0-387-34945-9
    ISBN (Print)978-1-5041-2958-9
    DOIs
    Publication statusPublished - 12 Oct 1995
    EventIFIP TC6 8th International Conference on Formal Description Techniques, FORTE 1995 - Montreal, Canada
    Duration: 17 Oct 199520 Oct 1995
    Conference number: 8

    Publication series

    NameIFIP Advances in Information and Communication Technology
    PublisherSpringer
    ISSN (Print)1868-4238
    ISSN (Electronic)1868-422X

    Conference

    ConferenceIFIP TC6 8th International Conference on Formal Description Techniques, FORTE 1995
    Abbreviated titleFORTE
    CountryCanada
    CityMontreal
    Period17/10/9520/10/95

    Keywords

    • Algebra
    • Communication
    • Information
    • Information processing
    • Telecommunications

    Fingerprint Dive into the research topics of 'Assertional verification of a connection management protocol'. Together they form a unique fingerprint.

    Cite this