This paper proposes a model-driven approach for the analysis of multimedia documents. Structural and behavioral properties of a multimedia document are veri ed thus guaranteeing its well-formedness and conformance before deployment. Multimedia documents are interpreted as object model instances of a multimedia document metamodel. Structural properties are veri ed using consistency reasoning over an ontology representation of the given object model together with OCL invariant validation (i.e., the application of OCL invariants to the given object model). Behavioral properties are veri ed through model checking on the transition system associated to the given multimedia document. Both metamodel and user-de ned behavioral properties are veri ed.
Multimedia documents describe applications as a set of components, which represent media objects, and relationships among them, which de ne temporal and real-time constraints over components. Declarative authoring languages may simplify the de nition of multimedia documents since they emphasize the description of a document rather than the implementation of its presentation.
Large multimedia documents, with many components, organized within quite rich and complex structures, may be ill-formed and fall victim of con icting relationships, leading to an application whose presentation is not what the author desires. An example of an ill-formed document includes cycles in composition nesting, where a composition is a group of components and relationships. Examples of undesired behavior (e.g. [7, 12, 13]) are the non-termination and/or unreachability of parts of a given document and the concurrent use of system resources, like an audio channel or a space at the screen. Usually, authors test their documents by executing them in an attempt to identify undesired behaviors, an approach which is not complete since not all possible behaviors may be explored on potentially ill-formed models.
Model-driven development (MDD) is a software development approach where models are the main artifacts of the development process. Models are represented as instances of metamodels, which describe the syntax of a modeling language, and may be used to derive di erent software artifacts, such as code in a programming language or even other models in di erent abstraction levels. This derivation process is called model transformation, which relates modeling languages through metamodels. Under that perspective, MDD is seen as a transformation between modeling languages applied to particular models, as shown in Figure 1, where M represents the concrete and M the abstract syntax of a source modeling language, N represents the concrete and N the abstract syntax of a target modeling language and the transformation between M and N . The operation parsing represents a mapping where a model m produces an instance m^ of M and pretty-printing represents the inverse mapping. The notation m 2 M denotes that model m is (syntactically) well-formed with respect to metamodel M .
The objective of MDD is to increase the abstraction level of the development process, so that authors may focus on modeling rather than implementation. In the context of multimedia documents, this is precisely the objective of NCL [9] and other multimedia authoring languages such as SMIL [15] and HTML5 [16]. Being language-driven, as shown in Figure 1, MDD ts very nicely with the development of multimedia applications in general and in particular with the validation of multimedia documents.
As previously mentioned, the veri cation of behavioral properties, like the ones presented before, is an important task in the development of multimedia applications, since it guarantees important properties of multimedia documents. Automaton based techniques t well in this type of veri cation through modelchecking [5] which essentially de nes a decision procedure for temporal formulae. The application of model checking to multimedia documents thus requires a formalization of its behavior as a labeled transition system (LTS) and a proper encoding of the desired behavioral properties as temporal formulae.
A question that arises then is: how to guarantee that the model being veri ed correctly represents the multimedia document?
Figure 2 shows MDD with the so-called transformation contracts [2{4]. A transformation contract is a speci cation of a model transformation de ned as a model that relates the metamodels of two modeling languages. Formally, a transformation contract K for a model transformation : M ! N is the disjoint union M onA N of the metamodels of the modeling languages together with associations in A between the model elements of M and N . The associations in A may be constrained by di erent kinds of properties, either structural or behavioral. The idea is that, following a design by contract style, every time a model transformation : M ! N is applied to a model m^ 2 M, rst the properties PM of the source metamodel are veri ed in m^, then properties PN of the target metamodel are veri ed in the generated model n^ = ( m^), together with the properties PK attached to the relations speci ed by A, which must hold on the joined model k = m^ onl n^ with l 2 A. The notation m j= PM means that the properties PM hold in model m, that is, m is in conformance with M.
An MDD process for the analysis of multimedia documents would re ne the process of Figure 2 by understanding M as the metamodel of a multimedia authoring language, such as NCL, and N as the metamodel of the speci cation language of a formal veri cation framework such as the speci cation language of a model checker.
This work proposes a transformation contract approach for the analysis of multimedia documents. Di erent veri cation techniques shall be used to analyze multimedia documents: (i) Consistency reasoning with description logic [1] will be used for verifying document consistency together with Object Constraint Language (OCL) invariant execution; and (ii) Linear Temporal Logic model checking appears to be the appropriate reasoning technique for behavioral properties of multimedia documents.
This work contributes with a general framework, with tool support, capable of analyzing di erent types of multimedia documents using di erent analysis (that is, veri cation and validation) techniques. Our proposal uses a languagedriven approach where the authoring language semantics is represented by a general model (called SHM - Simple Hypermedia Model) where structural and behavioral properties are veri ed. In this paper we outline our approach and discuss preliminary results achieved with a prototype of the tool.
The remainder of this paper is organized as follows. Section 2 presents the state-of-the-art on multimedia document analysis. Section 3 discusses the proposed solution for multimedia document analysis. Section 4 discusses the current state of the multimedia document analysis project illustrating preliminary results. Section 5 nishes this paper presenting the next steps of this work. 2
Santos et al. [13] presented an approach for the analysis of multimedia documents by translating it into a formal speci cation, in that case, into RT-LOTOS processes, using general mapping rules. The modularity and hierarchy of RT-LOTOS allows the combination of processes specifying the document presentation with other processes modeling the available platform.
The veri cation consists in the interpretation of the minimum reachability graph built from the formal speci cation, in order to prove if the action corresponding to the presentation end can be reached from the initial state. Each node in the graph represents a reachable state and each edge, the occurrence of an action or temporal progression. When a possible undesired behavior is found, the tool returns an error message to the author, so he can repair it. The tool in [13] could analyze NCM [14] and SMIL [15] documents.
Na and Furuta, in [12], presented caT (context aware Trellis), an authoring tool based on Petri nets. caT supports the analysis of multimedia documents by building the reachability tree of the analyzed document. The author de nes limit values for the occurrence of dead links (transitions that may not be triggered), places with token excess, besides other options, as the analysis maximum time. The tool investigates the existence of a terminal state, i.e., whether there is a state where no transitions are triggered. It also investigates the limitation property, i.e., if no place in the net has an unlimited number of tokens and the safeness property, i.e., if each place in the net has a token. The limitation analysis is important since tokens may represent scarce system resources.
Oliveira et al., in [7], presented HMBS (Hypermedia Model Based on Statecharts). An HMBS multimedia application is described by a statechart that represents its structural hierarchy, regarding nodes and links, and its humanconsumable components. Those components are expressed as information units, called pages and anchors. The statechart execution semantics provide the application navigation model. A statechart state is mapped into pages and transactions and events represent a set of possible link activations.
The statechart reachability tree for a speci c con guration may be used to verify if any page is unreachable, by verifying the occurrence of a state s in one of the generated con gurations, which indicate that the page is visible when the application navigation starts in the initial state considered. In a similar manner, it is possible to determine if a certain group of pages may be seen simultaneously searching state con gurations containing the states associated to those pages. The reachability tree also allows the detection of con gurations from which no other page may be reached or that present cyclical paths.
Junior et al., in [10], also present the veri cation of NCL documents through a model-driven approach. The veri cation is also achieved by transforming an NCL document into a Petri Net. This transformation is done in two steps. The rst step transforms the NCL document into a language called FIACRE, representing the document as a set of components and processes. Components represent media objects and compositions and processes represent the behavior associated to components. The second step transforms the FIACRE representation into a Petri Net. The veri cation uses a model-checking tool and temporal logic formulae to represent the behavior the author wants to verify. Once this work is very recent, the automation of that approach is a future work.
Our work contributes to the state-of-the-art with a general approach that can be used with di erent multimedia authoring languages.
We propose the use of the transformation contracts approach to analyze multimedia documents. Figure 3 re nes Figure 2 and illustrates our approach pictorially with NCL as the multimedia authoring language and Maude [6] as the speci cation language for formalizing multimedia documents. Informally, Maude modules are produced from NCL documents and the behavioral properties are represented as LTL formulae which are veri ed using the Maude model checker.
An important element of our approach is the so-called modeling language for the Simple Hypermedia Model (SHM) [8]. SHM models are important for two reasons: (i) they give formal meaning to NCM models, and (ii) should be a general formal representation for multimedia documents. SHM models are essentially transition systems that have basic elements to represent multimedia documents such as anchors as states, events as actions and links as transitions.From SHM models we could produce representations in di erent formalisms such as Maude or SMV [11]. Behavioral properties of well-formed models that hold the structural properties of a given authoring language are then checked at the concrete level such as Maude or SMV.
Let us go through each step of Figure 3. First, an NCL document is parsed into an NCM [14] model. (NCM is the conceptual model that NCL documents are based on and may be understood as its abstract syntax.) Thus, given an NCL document d, if (d^ = parse(d)) j= PN CM, that is, if the structural properties of NCM hold in d^ (such as non-circular nested compositions) then a model transformation N CM is applied on d^. Given that a proper SHM model s^ is produced by the application of the transformation contract from NCM to SHM, that is, essentially, its states are built properly from anchors, actions properly built from events and transitions properly built from links, a concrete representation of s^ may be produced in the speci cation language of the model checker, such as Maude.
d 2 NCL parsing d^ 2 N CM; ! d^ j= PN CM
NCM! ss^^ j2=SPHSHMM;; pretty-printin!g md 2 Maude
k j= PK
Given md, which is well-formed and in conformance with K = N CM onA SHM, one can now verify with a model-checker the temporal formulae that represent the behavioral properties exempli ed at the beginning of Section 1 (such as unreachability of document parts) and document speci c properties, dened by the document author and transformed into temporal formulae. Counterexamples produced by the model-checker, which are essentially traces that do not have the desired temporal formulae, may be presented back to the document author as sequences of links representing SHM transitions that correspond to transitions (or rewrites, in the case of Maude) of the faulty path encountered by the model checker. This process is illustrated pictorially in Figure 4, where d2NCL
! NCL author l2(NCLLinks ) NCL Analyzer = (parse(d)) ` modelCheck (s0; ) NCL Analyzer is the tool that essentially invokes the Maude model checker, represented in Figure 4 by the command modelCheck, which checks for the property (a conjunction of the behavioral properties together with author-de ned properties) using the speci cation (actually, rewrite theory) given by (parse(d)) using s0 as initial state (speci ed by the initial conditions of document d).
As mentioned before, SHM is intended to be a general multimedia model. The veri cation of multimedia documents speci ed with languages di erent from NCL, such as SMIL and HTML5, would require transformations from the abstract syntax of those languages to SHM together with a proper mapping from counter-examples of the chosen model-checker to the authoring language. The remaining of the analysis process is reused among those di erent languages.
We have a rst attempt at SHM and a prototype tool that transforms NCL to Maude modules. Section 4 brie y discusses preliminary results. 4
Part of the proposed solution is prototyped in a tool presented in [8], where the rst author, under the supervision of the remaining authors, proposed an implementation of a transformer from NCL documents to Maude modules. With that prototype it was possible to analyze structural and behavioral properties of NCL documents. Besides, the prototype gives us the intuition that the proposed solution seems to be appropriate.
The prototype was used in several small experiments with simple documents. Besides it was used with two non-trivial documents created by the Brazilian Digital TV community. A description of the two documents (\First Jo~ao" and \Live More") and their results are presented here.
\First Jo~ao" is an interactive TV application that presents an animation inspired in a chronicle about a famous Brazilian soccer player named Garrincha. It plays an animation, an audio and a background image. At the moment Garrincha dribbles the opponent, a video of kids performing the same dribble is presented and when his opponent falls on the ground, a photo of a kid in the same position is presented. The user may interact with the application pressing the red key at the moment a soccer shoes icon appears. The animation is resized and a video of a kid thinking about shoes starts playing.
This document was deployed by the authors of the NCL language as a sample document. As expected, the document is consistent with respect to the structural properties (PN CM), de ned taking into account the NCM grammar, and the behavioral properties (PSHM), from the set of parameterized properties. It was possible to verify that every anchor is reachable and has an end. Besides, the document as a whole ends.
\Live More" is an application that presents a TV show discussing health and welfare. Once the TV show starts playing, an interaction icon appears. If the user presses the red key of the remote control, four di erent food options appear. The user can choose a dish by pressing one of the colored keys of the remote control. When a dish is chosen, the TV user is informed about the quality of his choice, telling whether there are missing nutrients or nutrients in excess.
This document is consistent with respect to the structural properties (PN CM). However, the document is not consistent with respect to the behavioral properties (PSHM). It was possible to verify that once a dish is chosen, the anchor representing the chosen dish and its result do not end, and consequently the document as a whole.
The proposed prototype allows NCL document authors to verify if their document fails in one of the common undesired properties, besides validating the document structure. From the tests done with NCL documents it was possible to identify re nements in our Maude speci cation of SHM. Such re nements and open issues are addressed in the next section. 5
In this paper we presented an approach for the analysis of multimedia documents and a prototype tool that partially implements it. This section discusses future directions to our research project.
We are currently working on a re nement of the speci cation for SHM in [8], its Maude representation (to improve the e ciency of model checking it) and on a formal proof for the transformation N CM.
An important future work it to evaluate the generality of our approach, exploring mappings from di erent authoring languages to SHM, as indicated in the end of Section 3.
Our preliminary results consider prede ned properties representing patterns of behavior of multimedia documents (see Section 3.) We plan to incorporate user-de ned behavioral properties, by allowing the author to de ne such properties in a structured natural language (English, for example) that could be translated to LTL formulae.
We also consider evaluating the usability of the tool resulting from this
project using human-computer interaction techniques.
2. C. Braga. A transformation contract to generate aspects from access control
policies. Journal of Software and Systems Modeling, 10(3):395{409, 2010.
3. C. Braga, R. Menezes, T. Comicio, C. Santos, and E. Landim. On the speci
cation veri cation and implementation of model transformations with transformation
contracts. In 14th Brazilian Symposium on Formal Methods, volume 7021, pages
108{123, 2011.
4. C. Braga, R. Menezes, T. Comicio, C. Santos, and E. Landim. Transformation
contracts in practice. IET Software, 6(
http://www.itu.int/rec/T-REC-H.761-200904-S, 2009. 10. D. P. Junior, J. Farines, and C. A. S. Santos. Uma abordagem MDE para Modelagem e Veri caca~o de Documentos Multim dia Interativos. In WebMedia, 2011. in Portuguese. 11. K.L. McMillan. Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, 1993. 12. J.C. Na and R. Furuta. Dynamic documents: authoring, browsing, and analysis using a high-level petri net-based hypermedia system. In ACM Symposium on Document engineering, pages 38{47. ACM, 2001. 13. C.A.S. Santos, L.F.G. Soares, G.L. de Souza, and J.P. Courtiat. Design methodology and formal validation of hypermedia documents. In ACM International Conference on Multimedia, pages 39{48. ACM, 1998. 14. L. F. G. Soares, R. F. Rodrigues, and D. C. Muchaluat-Saade. Modeling, authoring and formatting hypermedia documents in the HyperProp system. Multimedia Systems, 2000. 15. W3C. Synchronized Multimedia Integration Language - SMIL 3.0 Speci cation.
http://www.w3c.org/TR/SMIL3, 2008. 16. W3C. HTML5: A vocabulary and associated APIs for HTML and XHTML. http://www.w3.org/TR/html5/, 2011.