Abstract
Authoring tools for editing hypermedia documents should be able to describe temporal and spatial relationships among objects, and user interactions as well. These tools can also support modifications in the document structure during the exhibition time. In all these situations, hypermedia document correctness should be guaranteed. In this paper, we describe an approach supporting the formal verification of documents in the Nested Context Language (NCL) and Synchronized Multimedia Integration Language (SMIL) standards. Using usual authoring tools, NCL and SMIL models are generated and, though an MDE design environment, transformed into formal verification models to be used following a method proposed in this paper and supported by an appropriate tool. A designer-oriented interface allows an easy and understandable description of properties to be checked and of required observers for more complex properties. The results of the verification are also presented in a comprehensive way for designers (as counterexamples) or executed step-by-step in a common displaying tool. Our approach allows designers to deal with the validation of their documents, built in a rigorous and consistent way, without prior knowledge of verification models and tools.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Allen, J.F.: Maintaining knowledge about temporal intervals. Commun. ACM 26, 832–843 (1983)
Asnawi, R., Ahmad, W.F.W., Rambli, D.R.A.: Formalization and verification of a live multimedia presentation model. International Journal of Computer Applications 20(2), Article 6 (2011)
ATLAS group: ATL user manual, version 0.7 (2006)
Berthomieu, B., Bodeveix, J.P., Farail, P., Filali, M., Garavel, H., Gaufillet, P., Lang, F., Vernadat, F.: FIACRE: an intermediate language for model verification in the topcased environment. In: 4th European Congress on Embedded RT Software - ERTS (2008)
Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA - construction of abstract state spaces for Petri Nets and Time Petri Nets. Int. Journal of Production Research 14(42), 2741–2756 (2004)
Bouyakoub, S., Belkhir, A.: SMIL builder: An incremental authoring tool for SMIL documents. ACM Trans. Multimedia Comp. Comm. Appl. 7, 2:1–2:30 (2011)
Bulterman, D., Hardman, L.: Structured multimedia authoring. ACM Trans. Multimedia Comput., Commun. and Appl. 1(1), 89–109 (2005)
Bulterman, D.C.A., Brailsford, D.F. (eds.): Proc. 2006 ACM Symposium on Document Engineering, Amsterdam, The Netherlands. ACM (2006)
Costa, R.M.D.R., Moreno, M.F., Soares, L.F.G.: Ginga-NCL: supporting multiple devices. In: Proc. of the XV Brazilian Symp. on MM and the Web, WebMedia 2009, pp. 6:1–6:8. ACM, USA (2009)
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 23(12), 1104–1123 (2000)
Felix, M., Haeusler, E., Soares, L.: Validating hypermedia documents: a timed automata approach. Monografias em Ciência da Computação, PUC-RioInf.MCC21/02, PUC-Rio, Brazil (2002)
Gaggi, O., Bossi, A.: Analysis and verification of SMIL documents. Multimedia Syst. 17(6), 487–506 (2011)
da Graça, C., Pimentel, M., Cattelan, R.G., Melo, E.L., do Prado, A.F., Teixeira, C.A.C.: End-user live editing of itv programmes. IJAMC 4(1), 78–103 (2010)
Henzinger, T., Manna, Z., Pnueli, A.: Timed transition systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 226–251. Springer, Heidelberg (1992)
ITU-T Recommendation H.761: Nested Context Language (NCL) and Ginga-NCL for IPTV Services (April 2009)
Laiola Guimarães, R., Monteiro de Resende Costa, R., Gomes Soares, L.F.: Composer: Authoring tool for iTV programs. In: Tscheligi, M., Obrist, M., Lugmayr, A. (eds.) EuroITV 2008. LNCS, vol. 5066, pp. 61–71. Springer, Heidelberg (2008)
Obeo: Acceleo user guide (2008), http://www.acceleo.org
Sampaio, P., Courtiat, J.P.: An approach for the automatic generation of RT-LOTOS specifications from SMIL 2.0 documents. J. Braz. Comp. Soc. 9(3), 39–51 (2004)
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 the 6th ACM Intl. Conf. on MM, pp. 39–48. ACM, USA (1998)
Schmidt, D.C.: Model-driven engineering. IEEE Computer 39(2), 25–31 (2006)
Yang, C.-C.: Detection of the time conflicts for SMIL-based multimedia presentations. In: Workshop on Computer Networks, Internet, and Multimedia, pp. 57–63. National Chung Cheng University, Taiwan (2000)
Yovine, S., Olivero, A., Monteverde, D., Cordoba, L., Reiter, G.: An approach for the verification of the temporal consistency of NCL applications. In: II Workshop de TV Digital Interativa (WTVDI) - Colocated with ACM WebMedia 2010 (2010)
Yu, H., He, X., Gao, S., Deng, Y.: Modeling and analyzing SMIL documents in SAM. In: Proc. 4th IEEE Int. Symp. on Multimedia Software Engineering, pp. 132–139. IEEE CS (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Picinin Júnior, D., Koliver, C., Santos, C.A.S., Farines, JM. (2014). Verifying Hypermedia Applications by Using an MDE Approach. In: Amyot, D., Fonseca i Casas, P., Mussbacher, G. (eds) System Analysis and Modeling: Models and Reusability. SAM 2014. Lecture Notes in Computer Science, vol 8769. Springer, Cham. https://doi.org/10.1007/978-3-319-11743-0_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-11743-0_12
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11742-3
Online ISBN: 978-3-319-11743-0
eBook Packages: Computer ScienceComputer Science (R0)