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
References in zbMATH (referenced in 3 articles )
Showing results 1 to 3 of 3.
- Bouyer, Patricia; Markey, Nicolas; Sankur, Ocan: Robust reachability in timed automata and games: a game-based approach (2015)
- André, Étienne; Liu, Yang; Sun, Jun; Dong, Jin-Song: Parameter synthesis for hierarchical concurrent real-time systems (2014)
- André, Étienne; Pellegrino, Giuseppe; Petrucci, Laure: Precise robustness analysis of time Petri nets with inhibitor ARCS (2013)