Modeling and Analyzing SMIL Documents in SAM

A composite multimedia object has specific timing relationships among the different types of component media. Coordinating the real-time presentation of information and maintaining the time-ordered relations among the component media is vital to satisfying quality of service (QoS) requirements. This paper proposes a formal approach to modeling and analyzing temporal aspects of SMIL documents using the Software Architecture Model (SAM), which is based on a dual formalism combining Petri nets and temporal logic. Synchronization elements of SMIL are systematically modeled by Petri nets. Useful QoS properties of SMIL documents are specified using temporal logic formulas and verified by automatic tools. Timelines of SMIL document presentation are analyzed by reachability tree technique.

• Type: Conference
• Year: 2002
• Where: MSE
• Authors: Huiqun Yu, Xudong He, Shu Gao, Yi Deng
• Keywords: Hardware, MSE 2002, Petri Nets, Smil Document, Temporal Logic