zbMATH — the first resource for mathematics

Quantitative robustness analysis of flat timed automata. (English) Zbl 1326.68185
Hofmann, Martin (ed.), Foundations of software science and computational structures. 14th international conference, FOSSACS 2011, held as part of the joint European conferences on theory and practice of software, ETAPS 2011, Saarbrücken, Germany, March 26 – April 3, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-19804-5/pbk). Lecture Notes in Computer Science 6604, 229-244 (2011).
Summary: Whereas formal verification of timed systems has become a very active field of research, the idealized mathematical semantics of timed automata cannot be faithfully implemented. Recently, several works have studied a parametric semantics of timed automata related to implementability: if the specification is met for some positive value of the parameter, then there exists a correct implementation. In addition, the value of the parameter gives lower bounds on sufficient resources for the implementation. In this work, we present a symbolic algorithm for the computation of the parametric reachability set under this semantics for flat timed automata. As a consequence, we can compute the largest value of the parameter for a timed automaton to be safe.
For the entire collection see [Zbl 1213.68041].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Uppaal; FLATA
Full Text: DOI