School of Computing

Automatic verification of a lip synchronisation protocol using UPPAAL

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

Formal Aspects of Computing, 10(5-6):550-575, August 1998 Special Issue on Formal Methods for Industrial Critical Systems.

Abstract

We present the formal specification and verification of a lip synchronisation algorithm using the real-time model checker UPPAAL. A number of specifications of this algorithm can be found in the literature, but this is the first automatic verification. We take a published specification of the algorithm, code it up in the UPPAAL timed automata notation and then verify whether the algorithm satisfies the key properties of jitter and skew. The verification reveals some flaws in the algorithm. In particular, it shows that for certain sound and video streams the algorithm can timelock before reaching a prescribed error state.



Bibtex Record

@article{710,
author = {H. Bowman and G. Faconti and J.-P. Katoen and D. Latella and M. Massink},
title = {Automatic Verification of a Lip Synchronisation Protocol using {UPPAAL}},
month = {August},
year = {1998},
pages = {550-575},
keywords = {multimedia, model checking, lip-synchronisation, timed automata},
note = {Special Issue on Formal Methods for Industrial Critical Systems.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/710},
    journal = {Formal Aspects of Computing},
    number = {5-6},
    publisher = {Springer-Verlag},
    volume = {10},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 23/06/2011 17:00