Shrinktech: a tool for the robustness analysis of timed automata. 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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element