Automatic verification of a lip-synchronisation protocol using Uppaal

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.

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:	Formal Methods and Tools (FMT)
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

Show download statistics for this publication

Repository Staff Only: item control page