The expressiveness power and flexibility of high-level authoring models (such as W3C SMIL 2.0 language) used for editing complex interactive multimedia documents can lead authors to specify inter-media synchronization relations that cannot be met at document presentation time, leading often the document presentation to a temporal deadlock, called a temporal inconsistency. To avoid these undesirable behaviors, a document formal design method is presented in this paper for identifying and then possibly correcting temporal inconsistencies. It is shown how the results of the verification phase can be used by a scheduling automaton for avoiding undesirable temporal inconsistencies at presentation time, as well as for generating a new document temporal model free from temporal inconsistency. The proposed method is instantiated for the SMIL 2.0 authoring model. The automatic translation of a SMIL 2.0 document into a RT-LOTOS specification is addressed. The formal verification of the RT-LOTOS specification is performed using RTL (the RT-LOTOS Laboratory) developed at LAAS-CNRS. The scheduling of the document presentation, taking into account all the document temporal non-determinism, is performed through the use of a new type of time automaton, called a TLSA (Time Labeled Scheduling Automaton). Potential state space explosion problems are addressed at the level of the translation between a SMIL 2.0 document and a RT-LOTOS specification. Simple examples illustrate the main concepts of the paper and the results achieved.


Formal Design Media Object Temporal Consistency Reachability Analysis Reachability Graph 
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.
    Courtiat, J.-P., Oliveira, R.C.: Proving temporal consistency in a new multimedia synchronization model. In: Proc of ACM Multimedia 1996, Boston, USA, pp. 141–152 (November 1996)Google Scholar
  2. 2.
    Santos, C.A.S., Soares, L.F.G., Souza, G.L., Courtiat, J.-P.: Design methodology and formal validation of hypermedia documents. In: Proc. of ACM Multimedia 1998, Bristol, UK, pp. 39–48 (September 1998)Google Scholar
  3. 3.
    Santos, C.A.S., Courtiat, J.-P., Saqui-Sannes, P.: A design methodology for the formal specification and verification of hypermedia documents. In: Proc. of FORTE/PSTV 1998, Paris, France. Chapman & Hall, Boca Raton (1998)Google Scholar
  4. 4.
  5. 5.
    Courtiat, J.P., Santos, C.A.S., Lohr, C., Outtaj, B.: Experience with RT-LOTOS, a temporal extension of the LOTOS formal description technique. Computer Communications (2000),
  6. 6.
    Yannakakis, M., Lee, D.: An efficient algorithm for minimizing real-time transition systems. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697. Springer, Heidelberg (1993)CrossRefGoogle Scholar
  7. 7.
  8. 8.
    Santos, C.A.S., Sampaio, P.N.M., Courtiat, J.-P.: Revisiting the concept of hypermedia document consistency. In: Proc of ACM Multimedia 1999, Orlando, USA (November 1999)Google Scholar
  9. 9.
    Lohr, C., Courtiat, J.P.: From the specification to the scheduling of time-dependent systems. In: Damm, W., Olderog, E.-R. (eds.) FTRTFT 2002. LNCS, vol. 2469, pp. 129–145. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  10. 10.
    Alur, R., Dill, D.L.: The theory of timed automata. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600. Springer, Heidelberg (1991)Google Scholar
  11. 11.
    Lohr, C.: Contribution à la conception de systèmes temps-réel s’appuyant sur la technique de description formelle RT-LOTOS, PhD Dissertation (in french), Université Paul Sabatier, Toulouse (December 2002) Google Scholar
  12. 12.
    Rutledge, L.: SMIL 2.0 – XML for Web Multimedia. IEEE Internet Computing, 78–84 (September-October 2001)Google Scholar
  13. 13.
    Jourdan, M.: A formal semantics of SMIL: a Web standard to describe multimedia documents. Computer Standards and Interfaces 23, 439–455 (2001)Google Scholar
  14. 14.
    Layaida, N., Keramane, C.: Mantaining Temporal Consistency of Multimedia Documents. In: Proc of ACM Workshop on Effective Abstractions in Multimedia, San Francisco (1995)Google Scholar
  15. 15.
    Sampaio, P.: Conception formelle de documents multimédia interactifs : une approche s’appuyant sur RT-LOTOS, PhD Dissertation (in french), Université Paul Sabatier, Toulouse (April 2003) Google Scholar
  16. 16.
    Léonard, L., Leduc, G.: An introduction to ET-LOTOS for the description of time-sensitive systems. Computer Networks and ISDN Systems 29, 271–292 (1997)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Jean-Pierre Courtiat
    • 1
  1. 1.LAAS – CNRSToulouseFrance

Personalised recommendations