Shrinktech: A tool for the robustness analysis of timed automata

Abstract

We present a tool for the robustness analysis of timed automata that can check whether a given time-abstract behaviour of a timed automaton is still present when the guards are perturbed. The perturbation model we consider is shrinking, which corresponds to increasing lower bounds and decreasing upper bounds in the clock guards by parameters. The tool synthesizes these parameters for which the given behaviour is preserved in the new automaton if possible, and generates a counter-example otherwise. This can be used for 1) robustness analysis, and for 2) deriving implementations under imprecisions. © 2013 Springer-Verlag.