Skip to main content
SpringerLink
Log in

Specification and verification of multimedia synchronization in Duration Calculus

  • Correspondence
  • Published:
Journal of Computer Science and Technology Aims and scope Submit manuscript

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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Chaochen Zhou, Hoare C A R, Ravn A. P. A calculus of durations.Information Processing Letters, 1991, 40(5): 269–276.

    Article  MATH  MathSciNet  Google Scholar 

  2. Hansen M R, Zhou Chaochen. Duration calculus: Logical foundations.Formal Aspects of Computing, 1997, 3: 283–330.

    Article  Google Scholar 

  3. Xu Qiwen, Yang Zhenyu. Derivation of control programs: A heating system. In4th International Conference on Hybrid-Systems, Ithaca, NY, USA, 1996.

  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.

  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.

  6. Allen J F. Maintaining knowledge about temporal intervals.Communications of the ACM, 1983, 26(11): 832–843.

    Article  MATH  Google Scholar 

  7. Anders P Ravn. Design of embedded real-time computing systems [Dissertation]. Department of Computer Science. Technical University of Denmark, October, 1995.

  8. Elisa Bertino, Elena Ferrari. Temporal synchronization models for multimedia data.IEEE Trans. Knowledge and Data Engineering, 1998, 10(4): 612–631.

    Article  Google Scholar 

  9. Pandya P K. DCVALID version 1.3 User Manual. Tata Institute of Fundamental Research, India, 1999.

  10. Buchanan M C, Zellweger P T. Specifying temporal behaviour in hypermedia documents. InProc. ACM Conf. Hypertext, Milan, 1992, pp.262–271.

  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.

  12. Ma Huadong, Kang G Shin. Checking consistency in multimedia synchronization constraints.IEEE Transaction on Multimedia, to appear.

  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.

    Article  Google Scholar 

  14. Naveed U Qazi, Miae Woo, Arif Ghafoor. A synchronization and communication model for distributed multimedia objects. InProc. ACM Multimedia93, 1993, pp.147–155.

  15. Petra Hoepner. Synchronizing the presentation of multimedia objects.Computer Communications, 1992, 15(9): 557–564.

    Article  Google Scholar 

  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.

  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.

    Article  Google Scholar 

  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.

    Article  MATH  MathSciNet  Google Scholar 

  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.

  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.

Download references

Author information

Authors and Affiliations

  1. School of Computer Science and Technology, Beijing University of Posts and Telecommunications, 100876, Beijing, P.R. China

    HuaDong Ma

Authors
  1. HuaDong Ma
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to HuaDong Ma.

Additional information

The work is supported by the National Natural Science Foundation of China under Grant Nos.69873006 and 60242002, UNU/HST Offshore Project and the Excellent Young Teachers Program of MOE, China.

Ma HuaDong is a professor of School of Computer Science and Technology, Beijing University of Posts and Telecommunications, China. He received his Ph.D. degree in computer science from Institute of Computing Technology. The Chinese Academy of Sciences in 1995, M.S. degree in computer science from Shenyang Institute of Computing Technology, The Chinese Academy of Sciences in 1990 and B.S. degree in mathematics from Henan Normal University in 1984. He visited UNU/HST as a research fellow in 1998 and 1999, respectively. From 1999 to 2000, he visited the Department of Electrical Engineering and Computer Science, The University of Michigan, USA. His research interests are multimedia, networking, ecommerce, computer animation and computer graphics. He has publised over 50 papers and 3 books on these fields.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Ma, H. Specification and verification of multimedia synchronization in Duration Calculus. J. Comput. Sci. & Technol. 18, 172–180 (2003). https://doi.org/10.1007/BF02948882

Download citation

  • Received:

  • Revised:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF02948882

Keywords

Search

Navigation