Discrete Timed Automata and MONA: Description, Specification and Verification of a Multimedia Stream

  • Rodolfo Gómez
  • Howard Bowman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2767)


MONA implements an efficient decision procedure for the weak second-order logic WS1S, and has already been applied in many non-trivial problems. Among these, we follow on from the work of Smith and Klarlund on the verification of a sliding-window protocol. This paper extends the scope of MONA to the verification of time-dependent protocols. We present Discrete Timed Automata (DTA) as a suitable formalism to specify and verify such protocols. In this paper our case study will be the specification and verification of a multimedia stream. DTA are as much influenced by IO Automata (syntactically) as they are by Timed Automata (semantically). A composition strategy is given to combine a set of synchronising automata, resulting in a product automaton over which safety properties can be verified. Invariance proofs are then performed inductively on the automaton structure. MONA supports the mechanical verification of invariance proofs.


Inference Rule Safety Property Label Transition System Media Stream Local Clock 
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.


  1. 1.
    Klarlund, N., Möller, A.: MONA Version 1.4 User Manual. BRICS, University of Aarhus, Denmark (2001) Google Scholar
  2. 2.
    Smith, M.A., Klarlund, N.: Verification of a Sliding Window Protocol using IOA and MONA. In: Bolognesi, T., Latella, D. (eds.) Formal Methods for Distributed System Development, pp. 19–34. Kluwer Academic Publishers, Dordrecht (2000)CrossRefGoogle Scholar
  3. 3.
    Lynch, N., Tuttle, M.: An introduction to input/output automata. CWI Quaterly 2, 219–246 (1989)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Sifakis, J., Yiovine, S.: Compositional specification of timed systems (extended abstract). In: Puech, C., Reischuk, R. (eds.) STACS 1996. LNCS, vol. 1046, pp. 347–359. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  5. 5.
    Bowman, H.: Time and action lock freedom properties for timed automata. In: Kim, S.K.M., Chin, B., Lee, D. (eds.) FORTE 2001, Formal Techniques for Networked and Distributed Systems, Cheju Island, Korea, pp. 119–134. Kluwer Academic Publishers, Dordrecht (2001)Google Scholar
  6. 6.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  7. 7.
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety. Springer, Heidelberg (1995)CrossRefzbMATHGoogle Scholar
  8. 8.
    Bowman, H., Faconti, G., Massink, M.: Specification and verification of media constraints using UPPAAL. In: 5th Eurographics Workshop on the Design, Specification and Verification of Interactive Systems, DSV-IS 1998. Eurographics Series. Springer, Heidelberg (1998)Google Scholar
  9. 9.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. International Journal on Software Tools for Technology Transfer 1, 134–152 (1997)CrossRefzbMATHGoogle Scholar
  10. 10.
    Gomez, R., Bowman, H.: A MONA-based Decision Procedure for Propositional Interval Temporal Logic. To appear in 4th. WITL, 15th. ESSLLI, Vienna (August 2003) Google Scholar
  11. 11.
    Pandya, P.K.: Specifying and deciding quantified discrete duration calculus formulae using DCVALID. Technical Report TCS00-PKP-1, Tata Institute of Fundamental Research (2000) Google Scholar
  12. 12.
    Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 571–586. Springer, Heidelberg (2002)Google Scholar
  13. 13.
    Blair, G., Blair, L., Bowman, H., Chetwynd, A.: Formal Specification of Distributed Multimedia Systems. University College London Press (1997)Google Scholar
  14. 14.
    Thomas, W.: Automata on Infinite Objects. In: Handbook of Theoretical Computer Science, vol. B, pp. 133–191. MIT Press, Cambridge (1990)Google Scholar
  15. 15.
    Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science, 183–235 (1994)Google Scholar
  16. 16.
    Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: specification. Springer, Heidelberg (1992)CrossRefzbMATHGoogle Scholar
  17. 17.
    Bowman, H., Faconti, G., Katoen, J.P., Latella, D., Massink, M.: Automatic verification of a lip synchronisation protocol using UPPAAL. Formal Aspects of Computing 10, 550–575 (1998)CrossRefzbMATHGoogle Scholar
  18. 18.
    Lynch, N., Vaandrager, F.: Forward and backward simulations—part ii: Timingbased systems. Information and Computation 128, 1–25 (1996)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Lamport, L.: Hybrid systems in TLA +. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 77–102. Springer, Heidelberg (1993)CrossRefGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Rodolfo Gómez
    • 1
  • Howard Bowman
    • 1
  1. 1.Computing LaboratoryUniversity of Kent at CanterburyCanterburyUK

Personalised recommendations