Robustness Analysis of Timed Automata

Symrob

Symrob is a tool for the robustness analysis (a.k.a. sensitivity or perturbation analysis) of real-time systems modeled as timed automata against safety specifications. In our setting, a timed automaton is robust if the specification holds even if the clocks can be assumed to be imprecise, up to an error bound to be computed. More formally, we model the imprecisions by "relaxing" all guards, e.g. replacing a guard a <= x <= b by a - δ <= x <= b+δ for unknown delta. Given a timed automaton in the Uppaal format, our tool synthesizes a value of delta under which the safety specification holds if there is a such a value.

The algorithm is presented in [Sankur 2015], and the formulation of the problem is based on [Puri 2000] and [De Wulf, Doyen, Markey, Raskin 2008].

Download (Linux)

Symrob 0.2 (28/06/2015) This version is fully written in OCaml, and does not use Verifix and Uppaal's libraries. It is equivalent to version 0.1, but it is easier to compile, and modify.

Symrob 0.1 (26/09/2014) source code, and binary. Licensed under GNU GPL 3.0.

Getting Started

As an example of usage, try the nonrobust.xml file in experiments directory. Type "symrob -e nonrobust.xml" to model check in the exact semantics, and just "symrob nonrobust.xml" for the robust semantics.

See also

The tool Verifix solves the same problem but does not provide any bound on tolerated imprecisions (see the TACAS15 paper below for performance comparison). Similar models of imprecisions are considered also in PyEcdar in the context of timed interfaces, using binary search on possible imprecision bounds.

References

[Sankur 2015] Symbolic Quantitative Robustness Analysis of Timed Automata. To appear in TACAS 2015.

[Puri 2000] Dynamical Properties of Timed Automata. Discrete Event Dynamic Systems 10(1-2): 87-113 (2000).

[De Wulf, Doyen, Markey, Raskin 2008] Robust safety of timed automata. Formal Methods in System Design 33(1-3): 45-84 (2008)