Automatic verification of a lip-synchronisation protocol using Uppaal

Share/Save/Bookmark

Bowman, H. and Faconti, G. and Katoen, J.P. and Latella, D. and Massink, M. (1998) Automatic verification of a lip-synchronisation protocol using Uppaal. Formal Aspects of Computing, 10 . pp. 550-575.

[img]PDF
Restricted to UT campus only
: Request a copy
183Kb
Abstract:We present the formal specification and verification of a lip-synchronisation protocol using the real-time model checker Uppaal. A number of specifications of this protocol can be found in the literature, but this is the first automatic verification. We take a published specification of the protocol, code it up in the Uppaal timed automata notation and then verify whether the protocol satisfies the key properties of jitter and skew. The verification reveals some aws 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.
Item Type:Article
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/63260
Official URL:http://dx.doi.org/10.1007/s001650050032
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page