Automatic verification of a lip-synchronisation protocol using Uppaal

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

doi:10.1007/s001650050032

Automatic verification of a lip-synchronisation protocol using Uppaal

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

Research output: Contribution to journal › Article › Academic › peer-review

19 Citations (Scopus)

7 Downloads (Pure)

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 language	English
Pages (from-to)	550-575
Number of pages	26
Journal	Formal aspects of computing
Volume	10
Issue number	5-6
DOIs	https://doi.org/10.1007/s001650050032
Publication status	Published - 1998

Keywords

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

Access to Document

10.1007/s001650050032

Cite this

@article{f56463194e7540f8b220322aa5af180c,

title = "Automatic verification of a lip-synchronisation protocol using Uppaal",

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.",

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

author = "H. Bowman and G. Faconti and J.-P. Katoen and D. Latella and M. Massink",

year = "1998",

doi = "10.1007/s001650050032",

language = "English",

volume = "10",

pages = "550--575",

journal = "Formal aspects of computing",

issn = "0934-5043",

publisher = "Springer",

number = "5-6",

}

TY - JOUR

T1 - Automatic verification of a lip-synchronisation protocol using Uppaal

AU - Bowman, H.

AU - Faconti, G.

AU - Katoen, J.-P.

AU - Latella, D.

AU - Massink, M.

PY - 1998

Y1 - 1998

N2 - 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.

AB - 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.

KW - FMT-RT: VERIFICATION OF REAL-TIME SYSTEMS

KW - FMT-MC: MODEL CHECKING

KW - Lip synchronisation

KW - UPPAAL

KW - Timed automata

KW - Specification

KW - Model checking

KW - Verification

U2 - 10.1007/s001650050032

DO - 10.1007/s001650050032

M3 - Article

SN - 0934-5043

VL - 10

SP - 550

EP - 575

JO - Formal aspects of computing

JF - Formal aspects of computing

IS - 5-6

ER -

Automatic verification of a lip-synchronisation protocol using Uppaal

Abstract

Keywords

Access to Document

Fingerprint

Cite this