About the semantic verification of SMIL documents

Author

Sampaio, P.N.M. ; Santos, C.A.S. ; Courtias, J.P.

Author_Institution

Lab. d´´Autom. et d´´Anal. des Syst., CNRS, Toulouse, France

Volume

3

fYear

2000

fDate

2000

Firstpage

1675

Abstract

The 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 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

Keywords

document handling; formal verification; graph theory; multimedia computing; reachability analysis; specification languages; RT-LOTOS formal description technique; RT-LOTOS specifications; SMIL documents; SMIL players; Synchronized Multimedia Integration Language; consistency properties; document presentation; erroneous semantic interpretations; formal approach; reachability analysis; reference behaviors; semantic verification; valid scheduling graph; Design methodology; Explosions; Page description languages; Proposals; Reachability analysis; State-space methods; Switches; Timing; XML;

fLanguage

English

Publisher

ieee

Conference_Titel

Multimedia and Expo, 2000. ICME 2000. 2000 IEEE International Conference on

Conference_Location

New York, NY

Print_ISBN

0-7803-6536-4

Type

conf

DOI

10.1109/ICME.2000.871093

Filename

871093