Specification and Verification of Media Constraints using UPPAAL
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.
KeywordsModel Checker Temporal Logic Media Object Media Stream Linear Time Temporal Logic
Unable to display preview. Download preview PDF.
- 2.V. Bellotti and A. MacLean. Integrating and communicating design perspectives with QOC design rationale. Technical Report ID/WP29, ESPRIT 7040 -AMODEUS, 1994.Google Scholar
- 3.Johan Bengtsson, W. O. David Griffioen, Kare J. Kristoffersen, Kim G. Larsen, Fredrik Larsson, Paul Pettersson, and Wang Yi. Verification of an audio protocol with bus collision using uppaal. In R. Alur and T. A. Henzinger, editors, Proceedings of the 8th International Conference on Computer-Aided Verification, LNCS 1102, pages 244–256, New Brunswick, New Jersey, USA, July 1996.Google Scholar
- 4.G.S. Blair, L. Blair, H. Bowman, and A. Chetwynd. Formal Specification of Distributed Multimedia Systems. University College London Press, September 1997.Google Scholar
- 5.M. Bordegoni, G. Faconti, S. Feiner, M. Maybury, T. Rist, S. Ruggieri, P. Trahanias, and M. Wilson. A standard reference model for intelligent presentation systems. Computer Standards and Interfaces, 1998.Google Scholar
- 6.H. Bowman, G. Faconti, J-P. Katoen, D. Latella, and M. Massink. Automatic verification of a lip synchronisation algorithm using UPPAAL. Accepted at FMICS’98, Amsterdam, The Netherlands, May 1998.Google Scholar
- 7.P.R. D’Argenio, J.-P. Katoen, T.C. Ruys, and J. Tretmans. The bounded retransmission protocol must be on time! In Proceedings of the 3rd International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, LNCS 1217, pages 416–431, Enschede, The Netherlands, April 1997.CrossRefGoogle Scholar
- 8.C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, LNCS1066. Springer-Verlag, 1996.Google Scholar
- 10.Klaus Havelund, Arne Skou, Kim G. Larsen, and Kristian Lund. Formal modelling and analysis of an audio/video protocol: An industrial case study using uppaal. In Proceedings of the 18th IEEE Real-Time Systems Symposium, pages 2–13, San Francisco, California, USA, 3–5 December 1997.Google Scholar
- 11.I. Herman, G. Reynolds, and J. Van Loo. PREMO: An emerging standard for multimedia, part i: Overview and framework. IEEE MultiMedia, 3:83–89, 1996.Google Scholar
- 12.Henrik Ejersbo Jensen, Kim G. Larsen, and Arne Skou. Modelling and analysis of a collision avoidance protocol using spin and uppaal. In Proceedings of the 2nd SPIN Workshop, Rutgers University, New Jersey, USA, August 1996.Google Scholar
- 15.Wang Yi, Paul Pettersson, and Mats Daniels. Automatic verification of real-time communicating systems by constraint solving. In Proceedings of the 7th International Conference on Formal Description Techniques, Berne, Switzerland, 4–7 October 1994.Google Scholar