Re-verification of a Lip Synchronization Algorithm using robust reachability

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

11 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 aspect 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 languageEnglish
Title of host publicationWorkshop on Formal Methods for Aerospace (FMA)
Place of PublicationManchester
PublisherManchester Institute for Mathematical Sciences
Number of pages14
Publication statusPublished - 3 Nov 2009
EventWorkshop on Formal Methods for Aerospace, FMA 2009: A workshop affiliated with Formal Methods Week (FM2009) - Eindhoven, Netherlands
Duration: 3 Nov 20093 Nov 2009

Workshop

WorkshopWorkshop on Formal Methods for Aerospace, FMA 2009
Abbreviated titleFMA
CountryNetherlands
CityEindhoven
Period3/11/093/11/09

Fingerprint

Synchronization
Jitter
Network protocols
Real time systems
Clocks
Testing

Keywords

  • METIS-264169
  • IR-69034
  • Timed Automata
  • EWI-16555
  • Formal Modelling
  • CR-F.4.3
  • Verification

Cite this

Kordy, P., Langerak, R., & Polderman, J. W. (2009). Re-verification of a Lip Synchronization Algorithm using robust reachability. In Workshop on Formal Methods for Aerospace (FMA) Manchester: Manchester Institute for Mathematical Sciences.
Kordy, Piotr ; Langerak, Rom ; Polderman, Jan Willem. / Re-verification of a Lip Synchronization Algorithm using robust reachability. Workshop on Formal Methods for Aerospace (FMA). Manchester : Manchester Institute for Mathematical Sciences, 2009.
@inproceedings{a1d8da35a1c041258365bc461adcfbe3,
title = "Re-verification of a Lip Synchronization Algorithm 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 aspect 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 = "METIS-264169, IR-69034, Timed Automata, EWI-16555, Formal Modelling, CR-F.4.3, Verification",
author = "Piotr Kordy and Rom Langerak and Polderman, {Jan Willem}",
year = "2009",
month = "11",
day = "3",
language = "English",
booktitle = "Workshop on Formal Methods for Aerospace (FMA)",
publisher = "Manchester Institute for Mathematical Sciences",
address = "United Kingdom",

}

Kordy, P, Langerak, R & Polderman, JW 2009, Re-verification of a Lip Synchronization Algorithm using robust reachability. in Workshop on Formal Methods for Aerospace (FMA). Manchester Institute for Mathematical Sciences, Manchester, Workshop on Formal Methods for Aerospace, FMA 2009, Eindhoven, Netherlands, 3/11/09.

Re-verification of a Lip Synchronization Algorithm using robust reachability. / Kordy, Piotr; Langerak, Rom; Polderman, Jan Willem.

Workshop on Formal Methods for Aerospace (FMA). Manchester : Manchester Institute for Mathematical Sciences, 2009.

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

TY - GEN

T1 - Re-verification of a Lip Synchronization Algorithm using robust reachability

AU - Kordy, Piotr

AU - Langerak, Rom

AU - Polderman, Jan Willem

PY - 2009/11/3

Y1 - 2009/11/3

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 aspect 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 aspect 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 - METIS-264169

KW - IR-69034

KW - Timed Automata

KW - EWI-16555

KW - Formal Modelling

KW - CR-F.4.3

KW - Verification

M3 - Conference contribution

BT - Workshop on Formal Methods for Aerospace (FMA)

PB - Manchester Institute for Mathematical Sciences

CY - Manchester

ER -

Kordy P, Langerak R, Polderman JW. Re-verification of a Lip Synchronization Algorithm using robust reachability. In Workshop on Formal Methods for Aerospace (FMA). Manchester: Manchester Institute for Mathematical Sciences. 2009