Ocan Sankur

Symrob

Symrob is a prototype tool for timed automata written in OCaml. It currently has two algorithms:

• Robustness 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].
• Abstraction-refinement algorithm using BDDs (the CUDD library). This algorithm is described in [Roussanaly, Sankur, Markey CAV 2019]

Download (Linux)

Latest version is on Github

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.

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

[Roussanaly, Sankur, Markey 2019] Abstraction Refinement Algorithms for Timed Automata CAV 2019.

[Sankur 2015] Symbolic Quantitative Robustness Analysis of Timed Automata. 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)