Advertisement

Journal of Computer Science and Technology

, Volume 18, Issue 2, pp 172–180 | Cite as

Specification and verification of multimedia synchronization in Duration Calculus

  • HuaDong Ma
Correspondence

Abstract

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

Keywords

liveness safety temporal synchronization duration calculus multimedia 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    Chaochen Zhou, Hoare C A R, Ravn A. P. A calculus of durations.Information Processing Letters, 1991, 40(5): 269–276.MATHCrossRefMathSciNetGoogle Scholar
  2. [2]
    Hansen M R, Zhou Chaochen. Duration calculus: Logical foundations.Formal Aspects of Computing, 1997, 3: 283–330.CrossRefGoogle Scholar
  3. [3]
    Xu Qiwen, Yang Zhenyu. Derivation of control programs: A heating system. In4th International Conference on Hybrid-Systems, Ithaca, NY, USA, 1996.Google Scholar
  4. [4]
    Dang Van Hung, Ko Kwang II. Verification via digitized model of real-time systems. InProc. IEEE Asia-Pacific Software Engineering Conference (APSEC'96), Seoul, 1996, pp.4–15.Google Scholar
  5. [5]
    Ma Huadong, Xu Qiwen, He Jifeng. Formal specification of multimedia synchronization protocols induration calculus. InProc. the First IEEE Pacific-Rim Conference on Multimedia, Sydney, Dec. 13–15, 2000, pp.124–129.Google Scholar
  6. [6]
    Allen J F. Maintaining knowledge about temporal intervals.Communications of the ACM, 1983, 26(11): 832–843.MATHCrossRefGoogle Scholar
  7. [7]
    Anders P Ravn. Design of embedded real-time computing systems [Dissertation]. Department of Computer Science. Technical University of Denmark, October, 1995.Google Scholar
  8. [8]
    Elisa Bertino, Elena Ferrari. Temporal synchronization models for multimedia data.IEEE Trans. Knowledge and Data Engineering, 1998, 10(4): 612–631.CrossRefGoogle Scholar
  9. [9]
    Pandya P K. DCVALID version 1.3 User Manual. Tata Institute of Fundamental Research, India, 1999.Google Scholar
  10. [10]
    Buchanan M C, Zellweger P T. Specifying temporal behaviour in hypermedia documents. InProc. ACM Conf. Hypertext, Milan, 1992, pp.262–271.Google Scholar
  11. [11]
    Ma Huadong, Kang G Shin. An approach to checking consistency in multimedia synchronization constraints.IEEE Int. Conf. Multimedia and Expro (ICME2000), New York, July 31–Aug. 2, 2000, pp. 1671–1674.Google Scholar
  12. [12]
    Ma Huadong, Kang G Shin. Checking consistency in multimedia synchronization constraints.IEEE Transaction on Multimedia, to appear.Google Scholar
  13. [13]
    Little T D C, Ghafoor A. Synchronization and storage models for multimedia objects.IEEE Journal of Selected Areas in Communications, 1990, 8(3): 413–427.CrossRefGoogle Scholar
  14. [14]
    Naveed U Qazi, Miae Woo, Arif Ghafoor. A synchronization and communication model for distributed multimedia objects. InProc. ACM Multimedia93, 1993, pp.147–155.Google Scholar
  15. [15]
    Petra Hoepner. Synchronizing the presentation of multimedia objects.Computer Communications, 1992, 15(9): 557–564.CrossRefGoogle Scholar
  16. [16]
    Herrtwich R G, Delgrossi L. ODA-based data modeling in multimedia systems.Technical Report TR 90-043, Int. Computer Science Inst., Berkeley, CA, 1990.Google Scholar
  17. [17]
    Ates A F, Bilgic Met al. Using timed CSP for specification, verification and simulation of multimedia synchronization.IEEE Journal of Selected Areas in Communications, 1996, 14(1): 126–137.CrossRefGoogle Scholar
  18. [18]
    Huadong Ma, Shenquan Liu. Multimedia data modeling based on temporal logic and XYZ system.Journal of Computer Science and Technology, 1999, 14(2): 188–193.MATHCrossRefMathSciNetGoogle Scholar
  19. [19]
    Liu Weimin, Ma Huadong. Modeling video-on-demand system in temporal logic.Lecture Notes in Computer Science, Vol.2195 (PCM2001), Springer, Oct., 2001, pp.983–988.Google Scholar
  20. [20]
    Courtiat J P, De Oliveira R C. Proving temporal consistency in a new multimedia synchronization model. InProc. ACM Multimedia96, Boston, 1996, pp.141–152.Google Scholar

Copyright information

© Science Press, Beijing China and Allerton Press Inc. 2003

Authors and Affiliations

  1. 1.School of Computer Science and TechnologyBeijing University of Posts and TelecommunicationsBeijingP.R. China

Personalised recommendations