Title :
Using timed CSP for specification verification and simulation of multimedia synchronization
Author :
Ates, Ahmet Feyzi ; Bilgic, Murat ; Saito, Senro ; Sarikaya, Behcet
Author_Institution :
Dept. of Comput. Sci., Univ. of Southern California, Los Angeles, CA, USA
fDate :
1/1/1996 12:00:00 AM
Abstract :
Timed communicating sequential processes (TCSP) language is used to specify fine-grain and coarse-grain multimedia synchronization. A lip synchronization system is an example of fine-grain synchronization. Several groupware scenarios are examples of coarse-grain synchronization. The formal specifications are used as the basis of verification and simulation. Safety and liveness timing requirements of the synchronization system are stated in terms of temporal logic formulas. Correctness analysis of the specification is shown using the temporal formulas and TCSP proof theory. It is shown that TCSP is powerful enough to be used in multimedia system design and verification. Next, simulation of multimedia synchronization is discussed. Various simulation models are developed for fine- and coarse-grain synchronization systems. It is shown that simulation modeling can lead to early detection of possible synchronization violations. The buffering requirements of a given synchronization mechanism can be effectively studied using simulation
Keywords :
communicating sequential processes; digital simulation; formal specification; multimedia communication; multimedia computing; simulation; synchronisation; temporal logic; TCSP proof theory; buffering requirements; coarse grain synchronization; correctness analysis; fine grain synchronization; formal specifications; groupware; lip synchronization system; multimedia communication; multimedia synchronization; multimedia system design; multimedia system verification; simulation modeling; simulation models; specification simulation; specification verification; synchronization system; synchronization violations detection; temporal logic formulas; timed communicating sequential processes language; timing requirements; Logic; Multimedia computing; Multimedia systems; Petri nets; Power system modeling; Real time systems; Safety; Specification languages; Streaming media; Timing;
Journal_Title :
Selected Areas in Communications, IEEE Journal on
