A Symbolic Algorithm for the Analysis of Robust Timed Automata

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

doi:10.1007/978-3-319-06410-9_25

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 proceeding › Conference contribution › Academic › peer-review

3 Citations (Scopus)

46 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 language	Undefined
Title of host publication	19th International Symposium on Formal Methods, FM 2014
Editors	C. Jones, P. Pihlajasaari, J.W. Sun
Place of Publication	London
Publisher	Springer
Pages	351-366
Number of pages	16
ISBN (Print)	978-3-319-06409-3
DOIs	https://doi.org/10.1007/978-3-319-06410-9_25
Publication status	Published - 2014
Event	19th International Symposium on Formal Methods - Singapore, Singapore Duration: 12 May 2014 → 16 May 2014 Conference number: 19th

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Verlag
Volume	8442
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	19th International Symposium on Formal Methods
Abbreviated title	FM 2014
Country/Territory	Singapore
City	Singapore
Period	12/05/14 → 16/05/14

Keywords

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

Access to Document

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

FM2014

Cite this

@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 ; 19th International Symposium on Formal Methods ; Conference date: 12-05-2014 Through 16-05-2014",

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",

address = "Germany",

}

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 et al.
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 proceeding › Conference contribution › Academic › peer-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 - Conference code: 19th

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

T2 - 19th International Symposium on Formal Methods

Y2 - 12 May 2014 through 16 May 2014

ER -