About the Semantic Verification of SMIL Documents

This paper presents a formal approach based on the RTLOTOS 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 behaviors for the presentation of a document. Also, some erroneous semantic interpretations of SMIL documents which are not conformant with their reference behaviors are illustrated using some currently available SMIL players.

• Type: Conference
• Year: 2000
• Where: ICMCS
• Authors: Paulo Nazareno Maia Sampaio, C. A. S. Santos, Jean-Pierre Courtiat
• Keywords: Formal Description Technique, ICMCS 2000, Multimedia, Reference Behaviors, SMIL Documents