The flexibility of high level authoring models (such as SMIL 2.0) for the edition of complex Interactive Multimedia Documents can lead authors, in certain cases, to specify synchronization relations which could not be satisfied during the presentation of the document, thus characterizing the occurrence of temporal inconsistencies. For this reason, we need to apply a methodology which provides the formal semantics for the dynamic behaviour of the document, consistency checking, and the scheduling of the presentation taking into account the temporal non-determinism of these documents. This paper refers to a methodology for the formal design of Interactive Multimedia Documents based on the formal description technique RT-LOTOS. In particular, this paper presents an approach applied by our methodology for the automatic translation of SMIL 2.0 documents into RT-LOTOS specifications.
A flexibilidade de modelos de autoria de alto nível (tais como o de SMIL 2.0) para a edição de Documentos Multimídia Interativos complexos pode levar os autores, em certos casos, a especificar relações de sincronização que não podem ser satisfeitas durante a apresentação do documento, caracterizando a ocorrência de inconsistências temporais. Por essa razão, é necessária a utilização de uma metodologia que ofereça uma semântica formal para o comportamento do documento, realize a verificação de consistência, o escalonamento e a apresentação levando em consideração o não-determinismo temporal desses documentos. Este artigo faz referência a uma metodologia para a concepção formal de Documentos Multimídia Interativos baseados na Técnica de Descrição Formal RT-LOTOS. Em particular, este artigo apresenta uma abordagem, utilizada pela nossa metodologia, para a tradução automática de documentos SMIL 2.0 em especificações RT-LOTOS.