Skip to main content

Automatic Verification of a Lip-Synchronisation Algorithm Using UPPAAL - Extended Version

Bowman, Howard and Faconti, Giorgio and Katoen, J-P. and Latella, D. and Massink, M. (1998) Automatic Verification of a Lip-Synchronisation Algorithm Using UPPAAL - Extended Version. In: Groote, J.F. and Luttik, B. and van Warnel, J., eds. FMICS'98, Third International Workshop on Formal Methods for Industrial Crtical Systems. CWI, pp. 97-124. ISBN 90-6196-480-6. (KAR id:21658)

Language: English
Download (535kB) Preview
[thumbnail of Automatic_Verification_of_a_Lip-Synchronisation_Algorithm_Using_UPPAAL_-_Extended_Version.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format


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.

Item Type: Book section
Additional information: 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.
Uncontrolled keywords: UPPAAL, Multimedia, Real-time, Formal Methods
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Mark Wheadon
Date Deposited: 22 Aug 2009 11:44 UTC
Last Modified: 16 Nov 2021 10:00 UTC
Resource URI: (The current URI for this page, for reference purposes)
Bowman, Howard:
  • Depositors only (login required):


Downloads per month over past year