An MDE approach for Modeling and Verification of Interactive Multimedia Documents
Abstract
This paper proposes a Model-Driven Engineering approach for modeling and verificating of interactive multimedia applications. The approach introduces a toolchain based on FIACRE language, that is used both as the target language of model transformation engines from NCL multimedia model, and as the source language of compilers into the targeted verification toolbox Tina. The paper illustrates the proposed approach with a case study of a NCL-based interactive TV application.
References
[1]
B. Berthomieu, J.-P. Bodeveix, P. Farail, M. Filali, H. Garavel, P. Gaufillet, F. Lang, and F. Vernadat. FIACRE: an intermediate language for model verification in the topcased environment. 4th European Congress on Embedded Real Time Software - ERTS, 2008.
[2]
B. Berthomieu, P.-O. Ribet, and F. Vernadat. The tool TINA - construction of abstract state spaces for petri nets and time petri nets. International Journal of Production Research, 14(42), 2004.
[3]
Bouyakoub Samia and Belkhir Abdelkader. Smil builder: An incremental authoring tool for smil documents. ACM Trans. Multimedia Comput. Commun. Appl., 7:2:1-2:30, February 2011.
[4]
M. C. Buchanan and P. T. Zellweger. Automatic temporal layout mechanisms revisited. ACM Trans. Multimedia Comput. Commun. Appl., 1:60-88, February 2005.
[5]
D. Bulterman and L. Hardman. Structured multimedia authoring. ACM Trans. Multimedia Comput., Commun. and Appl., 1(1):89-109, 2005.
[6]
Carlos de Sales Soares Neto, Luiz Fernando Gomes Soares, Rogério Ferreira Rodrigues and Simone Diniz Junqueira Barbosa. Construindo Programas Audiovisuais Interativos Utilizando NCL 3.0, 2010.
[7]
B. Combemale. Approche de metamodelisation pour la simulation et la verification de modele. IRIT Doctorate Thesis, 2008.
[8]
J.-P. Courtiat and R. C. De Oliveira. Proving temporal consistency in a new multimedia synchronization model. In Proceedings of the fourth ACM international conference on Multimedia, MULTIMEDIA -96, pages 141-152, New York, NY, USA, 1996. ACM.
[9]
J.-P. Courtiat, C. A. S. Santos, C. Lohr, and B. Outtaj. Experience with rt-lotos, a temporal extension of the lotos formal description technique. Computer Communications, pages 1104-1123, 2000.
[10]
P. Farail, P. Gaufillet, A. Canals, C. Le Camus, D. Sciamma, P. Michel, X. Cregut, M. Pantel, and F. Vernadat. The TOPCASED project: Toolkit in OPen-source for Critical Aplications and SystEms development. 3th European Congress on Embedded Real Time Software - ERTS, 2006.
[11]
R. Guimarães, R. D. R. Costa, and L. G. Soares. Composer: Authoring tool for itvprograms. In Euro iTV, Lecture Notes In Computer Science, vol. 5066., 2008.
[12]
N. Hirzalla, B. Falchuk, and A. Karmouch. A temporal model for interactive multimedia scenarios. IEEE MultiMedia, 2:24-31, July 1995.
[13]
C. Lohr and J.-P. Courtiat. From the specification to the scheduling of time-dependent systems. In Proceedings of the 7th International Symposium on Formal Techniques in Real-Time and Fault-Tolerant Systems: Co-sponsored by IFIP WG 2.2, FTRTFT-02, pages 129-146, London, UK, UK, 2002. Springer-Verlag.
[14]
M. F. Felix, E. H. Haeusler and L. F. G. Soares. Validating hypermedia documents: a timed automata approach. 2002.
[15]
Paulo Nazareno Maia Sampaio and Jean-Pierre Courtiat. An approach for the automatic generation of rt-lotos specifications from smil 2.0 documents. J. Braz. Comp. Soc., 9(3):39-51, 2004.
[16]
C. A. S. Santos and J.-P. Courtiat. Da Análise de Consistência à Formatação Temporal de um Documento Hipermídia Usando RT-LOTOS. SBMÍDIA, pages 63-78, 2000.
[17]
C. A. S. Santos, L. F. G. Soares, G. L. de Souza, and J.-P. Courtiat. Design methodology and formal validation of hypermedia documents. Proceedings of the sixth ACM international conference on Multimedia - MULTIMEDIA -98, pages 39-48, 1998.
[18]
Sergio Yovine, Alfredo Olivero, Daniel Monteverde, Laura Cordoba and Gabriel Reiter. An approach for the verification of the temporal consistency of ncl applications. In Simpósio Brasileiro de Sistemas Multimídia e Web (WebMedia), Belo Horizonte, Brasil, Outubro 2010.
[19]
L. Soares, R. Rodrigues, R. Cerqueira, and S. Barbosa. Variable and state handling in ncl. Multimedia Tools Appl., 50, December 2010.
[20]
L. F. G. Soares and S. D. J. Barbosa. Programando em NCL 3.0: desenvolvimento de aplicações para o middleware Ginga, TV Digital e Web. Elsevier, Rio de Janeiro, Brazil, 2009.
[21]
T. Tsang and R. Lai. Specification and verification of multimedia synchronization scenarios using time-estelle. Softw. Pract. Exper., 28:1185-1211, September 1998.
[22]
R. Willrich, P. de Saqui-Sannes, P. Sénac, and M. Diaz. Hypermedia document design using the htspn model. In MMM, pages 151-166, 1996.
Index Terms
- An MDE approach for Modeling and Verification of Interactive Multimedia Documents
Recommendations
Using MDE for the formal verification of embedded systems modeled by UML sequence diagrams
SBCCI '09: Proceedings of the 22nd Annual Symposium on Integrated Circuits and System Design: Chip on the DunesThis work presents a formal verification methodology that adopts concepts from Model Driven Engineering (MDE) for the automatic generation of a network of timed automata from the functional specification of an embedded application described using UML ...
An approach to verify live NCL applications
WebMedia '12: Proceedings of the 18th Brazilian symposium on Multimedia and the webThis paper describes a NCL 3.0 hypermedia application development toolchain which supports the verification of temporal and spatial consistency of NCL applications. In this toolchain, the application is translated into a TSS code and temporal logic ...
Towards a framework for executable systems modeling: an executable systems modeling language (ESysML)
Mod4Sim '18: Proceedings of the Model-driven Approaches for Simulation Engineering SymposiumThe Systems Modeling Language (SysML), which is the de-facto modeling standard in the systems engineering community, consists of a number of independently derived methodologies (i.e. state charts, activity diagrams etc.) which have been co-opted into a ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- FAPESC: Santa Catarina State Research and Innovation Support Foundation
- NICBR: Nucleo de Informatcao e Coordenacao do Ponto BR
- CGIBR: Comite Gestor da Internet no Brazil
- CAPES: Brazilian Higher Education Funding Council
- CNPq: National Council for Technological and Scientific Development
In-Cooperation
Publisher
Brazilian Computer Society
Porto Alegre, Brazil
Publication History
Published: 03 October 2011
Check for updates
Author Tags
Qualifiers
- Research-article
Acceptance Rates
WebMedia 2011 Paper Acceptance Rate 33 of 134 submissions, 25%;
Overall Acceptance Rate 270 of 873 submissions, 31%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 0Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 18 Jan 2025