Specification and Verification of Media Constraints using UPPAAL

Howard Bowman1, Giorgio P. Faconti2 and Meike Massink3

1Computing Lab., U. of Kent, Canterbury, Kent, CT2 7NF, UK

2CNR-Istituto CNUCE, Via S.Maria 36, 56126 - Pisa - Italy

3Dept. of Computer Science, U. of York, Heslington, York, YO1 5DD, UK

H.Bowman@ukc.ac.uk, G.Faconti@cnuce.cnr.it and M.Massink@guest.cnuce.cnr.it

Abstract

We present the formal specification and verification of a multimedia stream. The stream is described in a timed automata notation. We verify that the stream satisfies certain quality of service properties, in particular, throughput and end-to-end latency. The verification tool used is the real-time model checker UPPAAL.