PUMA
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.
 
 
Abstract
(English)
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
Specification
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