About the semantic verification of SMIL documents

This paper presents a formal approach based on the RT-LOTOS formal description technique for the semantic verification of SMIL documents. The reachability analysis of RT-LOTOS specifications provides the verification of consistency properties of a document and, later on, it also enables the generation of a valid scheduling graph for its presentation. This graph characterizes the reference behaviours for the presentation of a document. Also, some erroneous semantic interpretations of SMIL documents which are not conformant with their reference behaviours are illustrated using some currently available SMIL players.