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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [43 references]  Display  Hide  Download
https://hal.inria.fr/hal-01946641
Contributor : Tyrex Equipe <>
Submitted on : Wednesday, December 12, 2018 - 11:40:38 AM
Last modification on : Friday, October 25, 2019 - 1:32:16 AM
Long-term archiving on: Wednesday, March 13, 2019 - 12:35:49 PM

File

2018-10-ACM-TOMMa86-santos.pdf
Publisher files allowed on an open archive

Identifiers

Collections

CNRS | 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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

115

Files downloads

254

 

 

Contact

archive-ouverte@inria.fr