Specification and Verification of Multimedia Synchronization in Duration Calculus

This paper proposes a new method of specifying multimedia synchronization based on Duration Calculus (DC), a real time interval logic, presents thecompleteness of the new model, and uses it to specify the temporal relations betweenmultimedia objects. Moreover, the paper provides a method of constructing ameta-script based on basic synchronization requirements. Some properties ofthe formal specifications, including safety and liveness, are stated in DC.Furthermore, the verification of the above properties is discussed in DCsemantic. Compared with other methods for specifying multimediasynchronization, this method is more powerful and flexible, and it isgood at specifying the quantitative properties of multimedia synchronization.