Verifying Hypermedia Applications by Using an MDE Approach

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.