Re-verification of a Lip Synchronization Protocol using Robust Reachability

被引：1

作者：

Kordy, Piotr ^{[1
]}

Langerak, Rom ^{[1
]}

Polderman, Jan Willem ^{[2
]}

机构：

[1] Univ Twente, Formal Methods & Tools, Drienerlolaan 5, NL-7522 NB Enschede, Netherlands

[2] Univ Twente, Math Syst & Control Theory, NL-7522 NB Enschede, Netherlands

来源：

ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE | 2010年 / 20期

关键词：

D O I：

10.4204/EPTCS.20.5

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

The timed automata formalism is an importantmodel for specifying and analysing real-time systems. Robustness is the correctness of the model in the presence of small drifts on clocks or imprecision in testing guards. A symbolic algorithm for the analysis of the robustness of timed automata has been implemented. In this paper, we re-analyse an industrial case lip synchronization protocol using the new robust reachability algorithm. This lip synchronization protocol is an interesting case because timing aspects are crucial for the correctness of the protocol. Several versions of the model are considered: with an ideal video stream, with anchored jitter, and with non-anchored jitter.

引用

页码：49 / 62

页数：14

共 21 条

[1] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2]

Alur R., 1993, Proceedings of the Twenty-Fifth Annual ACM Symposium on the Theory of Computing, P592, DOI 10.1145/167088.167242

[3]

Alur R., 1993, LECTURE NOTES COMPUT, P209, DOI DOI 10.1007/3-540-57318-6

[4] Using timed CSP for specification verification and simulation of multimedia synchronization [J].

Ates, AF ;

Bilgic, M ;

Saito, S ;

Sarikaya, B .

IEEE JOURNAL ON SELECTED AREAS IN COMMUNICATIONS, 1996, 14 (01) :126-137

[5] Timed automata: Semantics, algorithms and tools [J].

Bengtsson, J ;

Yi, W .

LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 :87-124

[6]

Bowman H., 1998, Formal Aspects of Computing, V10, P550, DOI 10.1007/s001650050032

[7]

Daws C, 2006, LECT NOTES COMPUT SC, V4202, P143

[8]

De Wulf M, 2004, LECT NOTES COMPUT SC, V3253, P118

[9] Robust safety of timed automata [J].

De Wulf, Martin ;

Doyen, Laurent ;

Markey, Nicolas ;

Raskin, Jean-Francois .

FORMAL METHODS IN SYSTEM DESIGN, 2008, 33 (1-3) :45-84

[10]

Department of Information Technology at Uppsala University & the Department of Computer Science at Aalborg University, 2008, UPPAAL HOM PAG

← 1 2 3 →