Title :
Modeling and analyzing SMIL documents in SAM
Author :
Yu, Huiqun ; He, Xudong ; Gao, Shu ; Deng, Yi
Author_Institution :
Sch. of Comput. Sci., Florida Int. Univ., Miami, FL, USA
Abstract :
A composite multimedia object has specific timing relationships among the different types of component media. Coordinating the real-time presentation of information and maintaining time-ordered relations among the component media is vital for 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 using the reachability tree technique.
Keywords :
Internet; Petri nets; formal verification; multimedia computing; quality of service; real-time systems; software architecture; temporal logic; timing; Petri nets; QoS requirements; SAM; SMIL document analysis; SMIL document modeling; Software Architecture Model; automatic tools; composite multimedia object; formal approach; reachability tree technique; real-time information presentation; synchronization elements; temporal logic; time-ordered relations; timelines; timing relationships; Automatic logic units; Computer science; Connectors; Distributed computing; Helium; Multimedia computing; Petri nets; Quality of service; Software architecture; Timing;
Conference_Titel :
Multimedia Software Engineering, 2002. Proceedings. Fourth International Symposium on
Print_ISBN :
0-7695-1857-5
DOI :
10.1109/MMSE.2002.1181605
