A Hybrid Approach for Spatio-Temporal Validation of Declarative Multimedia Documents

Joel Dos Santos 1 Débora Muchaluat-Saade 2 Cécile Roisin 3 Nabil Layaïda 3
1 CEFET/RJ - Centro Federal de Educação Tecnológica Celso Suckow da Fonseca (Rio de Janeiro)
2 UFF - Universidade Federal Fluminense [Rio de Janeiro]
3 TYREX - Types and Reasoning for the Web
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : Declarative multimedia documents represent the description of multimedia applications in terms of media items and relationships among them. Relationships specify how media items are dynamically arranged in time and space during runtime. Although a declarative approach usually facilitates the authoring task, authors can still make mistakes due to incorrect use of language constructs or inconsistent or missing relationships in a document. In order to properly support multimedia application authoring, it is important to provide tools with validation capabilities. Document validation can indicate possible inconsistencies in a given document to an author so that it can be revised before deployment. Although very useful, multimedia validation tools are not often provided by authoring tools. This work proposes a multimedia validation approach that relies on a formal model called Simple Hypermedia Model (SHM). SHM is used for representing a document for the purpose of validation. An SHM document is validated using a hybrid approach based on two complementary techniques. The first one captures the document’s spatio-temporal layout in terms of its state throughout its execution by means of a rewrite theory, and validation is performed through model-checking. The second one captures the document’s layout in terms of intervals and event occurrences by means of Satisfiability Modulo Theories (SMT) formulas, and validation is performed through SMT solving. Due to different characteristics of both approaches, each validation technique complements the other in terms of expressiveness of SHM and tests to be checked. We briefly present validation tools that use our approach. They were evaluated with real NCL documents and by usability tests.
Type de document :
Article dans une revue
ACM Transactions on Multimedia Computing, Communications and Applications, Association for Computing Machinery, 2018, 14 (4), pp.1-24. 〈10.1145/3267127〉
Domaine :
Liste complète des métadonnées
https://hal.inria.fr/hal-01946641
Contributeur : Tyrex Equipe <>
Soumis le : mercredi 12 décembre 2018 - 11:40:38
Dernière modification le : jeudi 7 février 2019 - 16:58:52
Document(s) archivé(s) le : mercredi 13 mars 2019 - 12:35:49

Fichier

2018-10-ACM-TOMMa86-santos.pdf
Fichiers éditeurs autorisés sur une archive ouverte

Identifiants

Collections

LIG | INRIA | UGA

Citation

Joel Dos Santos, Débora Muchaluat-Saade, Cécile Roisin, Nabil Layaïda. A Hybrid Approach for Spatio-Temporal Validation of Declarative Multimedia Documents. ACM Transactions on Multimedia Computing, Communications and Applications, Association for Computing Machinery, 2018, 14 (4), pp.1-24. 〈10.1145/3267127〉. 〈hal-01946641〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

53

Téléchargements de fichiers

129

Contact


archive-ouverte@inria.fr