School of Computing

Automatic verification of a lip-synchronisation algorithm using uppaal - extended version

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

In Bas Luttick Jan Friso Groote and Jos Van Wamel, editors, FMICS'98, Third Internatinoal Workshop on Formal Methods for Industrial Crtical Systems, pages 182-196. CWI, May 1998 Also available as: H. Bowman, G. Faconti, J-P Katoen, D. Latella and M. Massink `Using UPPAAL for the Specification and Verification of a Lip-Sync Protocol' ERCIM Research Report 07/98-R054, July 1998.

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

@inproceedings{594,
author = {H. Bowman and G. Faconti and J-P. Katoen and D. Latella and M. Massink},
title = {Automatic Verification of a Lip-Synchronisation Algorithm Using UPPAAL - Extended Version},
month = {May},
year = {1998},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {Also available as: H. Bowman, G. Faconti, J-P Katoen, D. Latella and M. Massink `Using UPPAAL for the Specification and Verification of a Lip-Sync Protocol' ERCIM Research Report 07/98-R054, July 1998.},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1998/594},
    ISBN = {9061964806},
    booktitle = {FMICS'98, Third Internatinoal Workshop on Formal Methods for Industrial Crtical Systems},
    editor = {Jan Friso Groote, Bas Luttick and Jos Van Wamel},
    publisher = {CWI},
    refereed = {yes},
}

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

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

Last Updated: 21/03/2014