A Symbolic Algorithm for the Analysis of Robust Timed Automata

P.T. Kordy, Romanus Langerak, Sjouke Mauw, Jan W. Polderman

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

2 Citations (Scopus)
10 Downloads (Pure)

Abstract

We propose an algorithm for the analysis of robustness of timed automata, that is, the correctness of a model in the presence of small drifts of the clocks. The algorithm is an extension of the region based algorithm of Puri and uses the idea of stable zones as introduced by Daws and Kordy. Similarly to the assumptions made by Puri, we restrict our analysis to the class of timed automata with closed guards, progress cycles, and bounded clocks. We have implemented the algorithm and applied it to several benchmark specifications. The algorithm is a depth-first search based on on-the-fly reachability using zones.
Original languageUndefined
Title of host publication19th International Symposium on Formal Methods, FM 2014
EditorsC. Jones, P. Pihlajasaari, J.W. Sun
Place of PublicationLondon
PublisherSpringer
Pages351-366
Number of pages16
ISBN (Print)978-3-319-06409-3
DOIs
Publication statusPublished - 2014
Event19th International Symposium on Formal Methods - Singapore, Singapore
Duration: 12 May 201416 May 2014
Conference number: 19th

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Verlag
Volume8442
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Symposium on Formal Methods
Abbreviated titleFM 2014
CountrySingapore
CitySingapore
Period12/05/1416/05/14

Keywords

  • EWI-25008
  • Timed Automata
  • IR-91926
  • Verification
  • METIS-306004
  • Formal Modelling

Cite this

Kordy, P. T., Langerak, R., Mauw, S., & Polderman, J. W. (2014). A Symbolic Algorithm for the Analysis of Robust Timed Automata. In C. Jones, P. Pihlajasaari, & J. W. Sun (Eds.), 19th International Symposium on Formal Methods, FM 2014 (pp. 351-366). (Lecture Notes in Computer Science; Vol. 8442). London: Springer. https://doi.org/10.1007/978-3-319-06410-9_25
Kordy, P.T. ; Langerak, Romanus ; Mauw, Sjouke ; Polderman, Jan W. / A Symbolic Algorithm for the Analysis of Robust Timed Automata. 19th International Symposium on Formal Methods, FM 2014. editor / C. Jones ; P. Pihlajasaari ; J.W. Sun. London : Springer, 2014. pp. 351-366 (Lecture Notes in Computer Science).
@inproceedings{78804784332547c9afe1ff66898d843e,
title = "A Symbolic Algorithm for the Analysis of Robust Timed Automata",
abstract = "We propose an algorithm for the analysis of robustness of timed automata, that is, the correctness of a model in the presence of small drifts of the clocks. The algorithm is an extension of the region based algorithm of Puri and uses the idea of stable zones as introduced by Daws and Kordy. Similarly to the assumptions made by Puri, we restrict our analysis to the class of timed automata with closed guards, progress cycles, and bounded clocks. We have implemented the algorithm and applied it to several benchmark specifications. The algorithm is a depth-first search based on on-the-fly reachability using zones.",
keywords = "EWI-25008, Timed Automata, IR-91926, Verification, METIS-306004, Formal Modelling",
author = "P.T. Kordy and Romanus Langerak and Sjouke Mauw and Polderman, {Jan W.}",
note = "10.1007/978-3-319-06410-9_25",
year = "2014",
doi = "10.1007/978-3-319-06410-9_25",
language = "Undefined",
isbn = "978-3-319-06409-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "351--366",
editor = "C. Jones and P. Pihlajasaari and J.W. Sun",
booktitle = "19th International Symposium on Formal Methods, FM 2014",

}

Kordy, PT, Langerak, R, Mauw, S & Polderman, JW 2014, A Symbolic Algorithm for the Analysis of Robust Timed Automata. in C Jones, P Pihlajasaari & JW Sun (eds), 19th International Symposium on Formal Methods, FM 2014. Lecture Notes in Computer Science, vol. 8442, Springer, London, pp. 351-366, 19th International Symposium on Formal Methods, Singapore, Singapore, 12/05/14. https://doi.org/10.1007/978-3-319-06410-9_25

A Symbolic Algorithm for the Analysis of Robust Timed Automata. / Kordy, P.T.; Langerak, Romanus; Mauw, Sjouke; Polderman, Jan W.

19th International Symposium on Formal Methods, FM 2014. ed. / C. Jones; P. Pihlajasaari; J.W. Sun. London : Springer, 2014. p. 351-366 (Lecture Notes in Computer Science; Vol. 8442).

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

TY - GEN

T1 - A Symbolic Algorithm for the Analysis of Robust Timed Automata

AU - Kordy, P.T.

AU - Langerak, Romanus

AU - Mauw, Sjouke

AU - Polderman, Jan W.

N1 - 10.1007/978-3-319-06410-9_25

PY - 2014

Y1 - 2014

N2 - We propose an algorithm for the analysis of robustness of timed automata, that is, the correctness of a model in the presence of small drifts of the clocks. The algorithm is an extension of the region based algorithm of Puri and uses the idea of stable zones as introduced by Daws and Kordy. Similarly to the assumptions made by Puri, we restrict our analysis to the class of timed automata with closed guards, progress cycles, and bounded clocks. We have implemented the algorithm and applied it to several benchmark specifications. The algorithm is a depth-first search based on on-the-fly reachability using zones.

AB - We propose an algorithm for the analysis of robustness of timed automata, that is, the correctness of a model in the presence of small drifts of the clocks. The algorithm is an extension of the region based algorithm of Puri and uses the idea of stable zones as introduced by Daws and Kordy. Similarly to the assumptions made by Puri, we restrict our analysis to the class of timed automata with closed guards, progress cycles, and bounded clocks. We have implemented the algorithm and applied it to several benchmark specifications. The algorithm is a depth-first search based on on-the-fly reachability using zones.

KW - EWI-25008

KW - Timed Automata

KW - IR-91926

KW - Verification

KW - METIS-306004

KW - Formal Modelling

U2 - 10.1007/978-3-319-06410-9_25

DO - 10.1007/978-3-319-06410-9_25

M3 - Conference contribution

SN - 978-3-319-06409-3

T3 - Lecture Notes in Computer Science

SP - 351

EP - 366

BT - 19th International Symposium on Formal Methods, FM 2014

A2 - Jones, C.

A2 - Pihlajasaari, P.

A2 - Sun, J.W.

PB - Springer

CY - London

ER -

Kordy PT, Langerak R, Mauw S, Polderman JW. A Symbolic Algorithm for the Analysis of Robust Timed Automata. In Jones C, Pihlajasaari P, Sun JW, editors, 19th International Symposium on Formal Methods, FM 2014. London: Springer. 2014. p. 351-366. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-06410-9_25