Skip to main content
Kent Academic Repository

Automatic Verification of a Lip Synchronisation Protocol using UPPAAL

Bowman, Howard, Faconti, Giorgio, Katoen, J-P., Latella, D., Massink, M. (1998) Automatic Verification of a Lip Synchronisation Protocol using UPPAAL. Formal Aspects of Computing, 10 (5-6). pp. 550-575. ISSN 1433-299X. (doi:10.1007/s001650050032) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:21620)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://dx.doi.org/10.1007/s001650050032

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.

Item Type: Article
DOI/Identification number: 10.1007/s001650050032
Additional information: Special Issue on Formal Methods for Industrial Critical Systems.
Uncontrolled keywords: multimedia, model checking, lip-synchronisation, timed automata
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 22:39 UTC
Last Modified: 16 Nov 2021 10:00 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/21620 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.