Istituto di Scienza e Tecnologie dell'Informazione     
Bowman H., Faconti G., Kaoten J., Latella D., Massink M. Automatic verification of a lip synchronisation protocol using UPPAAL. In: Formal Aspects of Computing, vol. 10 pp. 550 - 575. BCS, 1999.
We present the formal speci cation and veri cation of a lip-synchronisation protocol using the real-time model checker Uppaal. A number of speci cations of this protocol can be found in the literature, but this is the rst automatic veri cation. We take a published speci cation of the protocol, code it up in the Uppaal timed automata notation and then verify whether the protocol satis es the key properties of jitter and skew. The veri cation reveals some flaws in the protocol. In particular, it shows that for certain sound and video streams the protocol can time-lock before reaching a prescribed error state. We also discuss our experience with Uppaal, with particular reference to modelling timeouts and to deadlock analysis.
Subject Model checking
Lip synchronisation
F.1.1 Models of Computation

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional