Analysis and verification of SMIL documents

In this paper, we consider the problem of automatic verification of SMIL documents and present a tool which can assist the user in the complex task of authoring a multimedia presentation. The tool is based on a formal semantics defining the temporal aspects of SMIL elements by means of a set of inference rules. The rules, in the spirit of Hoare’s semantics, describe how the execution of a piece of code changes the state of the computation of a player. If any temporal conflict is found, the system returns a message to the user pointing out the element which contains the conflict and its motivation. This helps the user to develop robust and clear code.