Abstract.
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.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
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)
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)
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)
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), http://www.laas.fr/RT-LOTOS
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)
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)
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)
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)
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)
Rutledge, L.: SMIL 2.0 – XML for Web Multimedia. IEEE Internet Computing, 78–84 (September-October 2001)
Jourdan, M.: A formal semantics of SMIL: a Web standard to describe multimedia documents. Computer Standards and Interfaces 23, 439–455 (2001)
Layaida, N., Keramane, C.: Mantaining Temporal Consistency of Multimedia Documents. In: Proc of ACM Workshop on Effective Abstractions in Multimedia, San Francisco (1995)
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)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 IFIP International Federation for Information Processing
About this paper
Cite this paper
Courtiat, JP. (2003). Formal Design of Interactive Multimedia Documents. In: König, H., Heiner, M., Wolisz, A. (eds) Formal Techniques for Networked and Distributed Systems - FORTE 2003. FORTE 2003. Lecture Notes in Computer Science, vol 2767. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39979-7_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-39979-7_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20175-5
Online ISBN: 978-3-540-39979-7
eBook Packages: Springer Book Archive