© University of Kent - Contact | Feedback | Legal | FOI | Cookies
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}, }