Re-verification of a Lip Synchronization Protocol using Robust Reachability

P.T. Kordy; L.M. Bujorianu; Romanus Langerak; Michael Fischer; Jan W. Polderman

doi:10.4204/EPTCS.20.5

Re-verification of a Lip Synchronization Protocol using Robust Reachability

P.T. Kordy, L.M. Bujorianu (Editor), Romanus Langerak, Michael Fischer (Editor), Jan W. Polderman

Research output: Contribution to journal › Article › Academic › peer-review

5 Citations (Scopus)

127 Downloads (Pure)

Abstract

The timed automata formalism is an important model 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.

Original language	Undefined
Pages (from-to)	49-62
Number of pages	14
Journal	Electronic proceedings in theoretical computer science
Volume	20
DOIs	https://doi.org/10.4204/EPTCS.20.5
Publication status	Published - 2010
Event	Workshop on Formal Methods for Aerospace, FMA 2009: A workshop affiliated with Formal Methods Week (FM2009) - Eindhoven, Netherlands Duration: 3 Nov 2009 → 3 Nov 2009

Keywords

IR-75784
EWI-19407
METIS-277505

Access to Document

10.4204/EPTCS.20.5

Cite this

@article{5c6d92a7ba3d49469ab28f074b0349eb,

title = "Re-verification of a Lip Synchronization Protocol using Robust Reachability",

abstract = "The timed automata formalism is an important model 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.",

keywords = "IR-75784, EWI-19407, METIS-277505",

author = "P.T. Kordy and L.M. Bujorianu and Romanus Langerak and Michael Fischer and Polderman, {Jan W.}",

note = "10.4204/EPTCS.20.5 ; Workshop on Formal Methods for Aerospace, FMA 2009 ; Conference date: 03-11-2009 Through 03-11-2009",

year = "2010",

doi = "10.4204/EPTCS.20.5",

language = "Undefined",

volume = "20",

pages = "49--62",

journal = "Electronic proceedings in theoretical computer science",

issn = "2075-2180",

publisher = "Open Publishing Association",

}

TY - JOUR

T1 - Re-verification of a Lip Synchronization Protocol using Robust Reachability

AU - Kordy, P.T.

AU - Langerak, Romanus

AU - Polderman, Jan W.

A2 - Bujorianu, L.M.

A2 - Fischer, Michael

N1 - 10.4204/EPTCS.20.5

PY - 2010

Y1 - 2010

N2 - The timed automata formalism is an important model 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.

AB - The timed automata formalism is an important model 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.

KW - IR-75784

KW - EWI-19407

KW - METIS-277505

U2 - 10.4204/EPTCS.20.5

DO - 10.4204/EPTCS.20.5

M3 - Article

SN - 2075-2180

VL - 20

SP - 49

EP - 62

JO - Electronic proceedings in theoretical computer science

JF - Electronic proceedings in theoretical computer science

T2 - Workshop on Formal Methods for Aerospace, FMA 2009

Y2 - 3 November 2009 through 3 November 2009

ER -