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: | 05 Nov 2024 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
Bowman, Howard.
| Creator's ORCID: |
 https://orcid.org/0000-0003-4736-1869
|
|---|---|
| CReDIT Contributor Roles: |
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):
Altmetric
Altmetric
