Automatic verification of a lip-synchronisation protocol using Uppaal

H. Bowman, G. Faconti, J.-P. Katoen, D. Latella, M. Massink

    Research output: Contribution to journalArticleAcademicpeer-review

    18 Citations (Scopus)

    Abstract

    We present the formal specification and verification of a lip-synchronisation protocol using the real-time model checker Uppaal. A number of specifications of this protocol can be found in the literature, but this is the first automatic verification. We take a published specification of the protocol, code it up in the Uppaal timed automata notation and then verify whether the protocol satisfies the key properties of jitter and skew. The verification reveals some aws in the protocol. In particular, it shows that for certain sound and video streams the protocol can time-lock before reaching a prescribed error state. We also discuss our experience with Uppaal, with particular reference to modelling timeouts and to deadlock analysis.
    Original languageEnglish
    Pages (from-to)550-575
    Number of pages26
    JournalFormal aspects of computing
    Volume10
    Issue number5-6
    DOIs
    Publication statusPublished - 1998

    Keywords

    • FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS
    • FMT-MC: MODEL CHECKING
    • Lip synchronisation
    • UPPAAL
    • Timed automata
    • Specification
    • Model checking
    • Verification

    Fingerprint Dive into the research topics of 'Automatic verification of a lip-synchronisation protocol using Uppaal'. Together they form a unique fingerprint.

    Cite this