期刊文献+

Specification and Verification of Multimedia Synchronization in Duration Calculus 被引量:2

原文传递
导出
摘要 This paper proposes a new method of specifying multimedia synchronization basedon 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 paperprovides a method of constructing a meta-script based on basic synchronization requirements. Someproperties of the formal specifications, including safety and liveness, are stated in DC. Furthermore,the verification of the above properties is discussed in DC semantic. Compared with other methodsfor specifying multimedia synchronization, this method is more powerful and flexible, and it is goodat specifying the quantitative properties of multimedia synchronization.
作者 马华东
出处 《Journal of Computer Science & Technology》 SCIE EI CSCD 2003年第2期172-180,共9页 计算机科学技术学报(英文版)
基金 国家自然科学基金,教育部优秀青年教师资助计划
  • 相关文献

参考文献20

  • 1Zhou Chaochen, Hoare C A R, Ravn A P. A calculus of durations. Information Processing Letters, 1991, 40(5):269-276.
  • 2Hansen M R, Zhou Chaochen. Duration calculus: Logical foundations. Formal Aspects of Computing, 1997, 3: 283-330.
  • 3Xu Qiwen, Yang Zhenyu. Derivation of control programs: A heating system. In 4th International Conference on Hybrid Systems, Ithaca, NY, USA, 1996.
  • 4Dang Van Hung, Ko Kwang Il. Verification via digitized model of real-time systems. In Proc. IEEE Asia-Pacific Software Engineering Conference (APSEC'96), Seoul, 1996, pp.4-15.
  • 5Ma Huadong, Xu Qiwen, He Jifeng. Formal specification of multimedia synchronization protocols in duration calculus. In Proc. the First IEEE Pacific-Rim Conference on Multimedia, Sydney, Dec. 13-15, 2000, pp. 124-129.
  • 6Allen J F. Maintaining knowledge about temporal intervals. Communications of the ACM, 1983, 26(11): 832-843.
  • 7Anders P Ravn. Design of embedded real-time computing systems [Dissertation]. Department of Computer Science, Technical University of Denmark, October, 1995.
  • 8Elisa Bertino, Elena Ferrari. Temporal synchronization models for multimedia data. IEEE Trans. Knowledge and Data Engineering, 1998, 10(4): 612-631.
  • 9Pandya P K. DCVALID version 1.3 User Manual. Tara Institute of Fundamental Research, India, 1999.
  • 10Buchanan M C, Zellweger P T. Specifying temporal behaviour in hypermedia documents. In Proc. ACM Conf.Hypertext, Milan, 1992, pp.262-271.

同被引文献10

  • 1焦燕鸿,侯自强,张宇.Mobile SIP与Mobile IP的比较[J].北京邮电大学学报,2004,27(z1):62-66. 被引量:4
  • 2Duan L, Wu W L. Mobility and QoS support in mobile IP networks[J]. Journal of China Universities of Posts and Telecommunications, 2004, 11(1) : 60-67.
  • 3Park T, Dadej A. OPNET simulation modeling and analysis of enhanced Mobile IP[A]. Proceeding IEEE WCNC 2003[C]. IEEE Press, 2003. 1017-1024.
  • 4Dang Z. Using the ASTRAL model checker to analyze mobile IP[A]. ICSE'99[C]. 1999. 132-141.
  • 5IETF. RFC 2002-1996, IP mobility support[S].
  • 6Alur R, Dill D. A theory of timed automata[J]. Journal of Theoretical Computer Science, 1994, 126 (2) : 183-235.
  • 7Larsen K G, Pettersson P, Wang Y. Uppaal in a nutshell [J ]. Journal on Software Tools for Technology Transfer, 1997, 1(1-2): 134-152.
  • 8叶敏华,张惠民,刘雨.异种网络间的Mobile IP切换问题[J].北京邮电大学学报,2002,25(3):83-87. 被引量:9
  • 9张泽莉,马华东.简单网络支付协议的形式模型[J].北京邮电大学学报,2002,25(4):42-46. 被引量:1
  • 10赵宇虹,艾波.一种用基本ASM定义SDL静态语义的方法[J].北京邮电大学学报,2004,27(1):55-59. 被引量:1

引证文献2

二级引证文献2

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部