Using timed CSP for specification verification and simulation of multimedia synchronization

被引：24

作者：

Ates, AF

Bilgic, M

Saito, S

Sarikaya, B

机构：

[1] UNIV SO CALIF,DEPT COMP SCI,LOS ANGELES,CA 90089

[2] NETAS DMS PLANNING DEPT R814,ISTANBUL 81244,TURKEY

[3] UNIV AIZU,COMP COMMUN LAB,FUKUSHIMA 96580,JAPAN

来源：

IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS | 1996年 / 14卷 / 01期

关键词：

timed CSP; temporal logic; multimedia synchronization; temporal interval; live source; stored object; simulation;

D O I：

10.1109/49.481699

中图分类号：

TM [电工技术]; TN [电子技术、通信技术];

学科分类号：

0808 ; 0809 ;

摘要：

Timed Communicating Sequential Processes (TCSP) language is used to specify fine-grain and coarse-grain multimedia synchronization. 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, Buffering requirements of a given synchronization mechanism can be effectively studied using simulation.

引用

页码：126 / 137

页数：12

共 19 条

[1]

BLAIR GS, 1992, MPG9245 LANC U DEP C

[2]

BLAIR GS, 1993, FORMAL SUPPORT SPECI

[3]

COURTIAT JP, 1994, ICMCS 94 BOSTON, P173

[4]

DAVIES J, 1992, PRG96 OXF U PROGR RE

[5]

DAVIES J, 1991, LECT NOTES COMPUTER, V600, P640

[6]

DEMEER J, 1994, PROTOCOL SPECIFICATI, P139

[7]

DIAZ M, 1994, ANN TELECOMMUNIC MAY

[8] A RELY AND GUARANTEE METHOD FOR TIMED CSP - A SPECIFICATION AND DESIGN OF A TELEPHONE EXCHANGE [J].

KAY, A ;

REED, JN .

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1993, 19 (06) :625-639

[9]

LI L, 1994, ACM SPRINGER MULTIME, V1, P154

[10]

LI L, 1994, ACM SPRINGER MULTIME, V1, P143

← 1 2 →