Specification and Verification of Media Constraints using UPPAAL

  • Howard Bowman
  • Giorgio P. Faconti
  • Mieke Massink
Part of the Eurographics book series (EUROGRAPH)


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.


Model Checker Temporal Logic Media Object Media Stream Linear Time Temporal Logic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, (126):183–235, 1994.MathSciNetMATHCrossRefGoogle Scholar
  2. 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. 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. 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. 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. 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. 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. 8.
    C. Daws, A. Olivero, S. Tripakis, and S. Yovine. The tool KRONOS. In Hybrid Systems III, LNCS1066. Springer-Verlag, 1996.Google Scholar
  9. 9.
    P.G. Harrison and N.M. Patel. Performance Modelling of Communication Networks and Computer Architectures. Addison-Wesley, 1993.MATHGoogle Scholar
  10. 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. 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. 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
  13. 13.
    Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.CrossRefGoogle Scholar
  14. 14.
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.MATHGoogle Scholar
  15. 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

Copyright information

© Springer-Verlag Wien 1998

Authors and Affiliations

  • Howard Bowman
    • 1
  • Giorgio P. Faconti
    • 2
  • Mieke Massink
    • 3
  1. 1.Computing Lab.U. of KentCanterburyUK
  2. 2.CNR-Istituto CNUCEPisaItaly
  3. 3.Dept. of Computer ScienceU. of YorkHeslingtonUK

Personalised recommendations