loading...
Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol
Macao, China December 04-December 07
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/APSEC.2001.991504Eighth Asia-Pacific Software Engineer ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Duration Calculus DC), an extension of interval temporal logic, has been shown very powerful and suitable for specifying multimedia protocols. Generally speaking, it is impossible to verify the DC specifications using model-checking because of DC's undecidability. H. Dierks presented an approach to solving the problem. The main contribution of this paper is improving H. Dierks's algorithm so that it can be used to transform the DC specification of multimedia protocols to the input of the model checker. The basic idea behind this work is that we use general DC To specify multimedia protocols, and the improved H. Dierks' algorithm to transform them to PLC-Automata, further to Timed Automata. Using model-checkers developed for TA, we can verify the correctness of protocols. We shall demonstrate it by Adaptive LSP. For convenience, we use more general forms of DC Implementables, but they can be reduced to the four standard forms given by H. Dierks.
Index Terms:
Synthesis, Lip Synchronisation Protocol, Timed Automata, Duration Calculus, Multimedia.
Citation:
Huadong Ma, Liang Li, Jianzhong Wang, Naijun Zhan, "Automatic Synthesis of the DC Specifications of Lip Synchronisation Protocol," apsec, pp.371, Eighth Asia-Pacific Software Engineering Conference (APSEC'01), 2001
Usage of this product signifies your acceptance of the Terms of Use.