The shrinktech Tool

The Shrinktech Tool

Shrinktech is a tool for robustness analysis of timed automata based on the results described in [SBM14]. A tool paper was presented in [San13].

The tool can be used to check whether a given timed automaton is robust to guard shrinkings: whether the behaviour is preserved when all guards of the form l <= x <= u, are transformed to l+delta <= x <= u-delta', for some unknown values delta, delta'. Each atomic guard is shrunk by different parameters, and the tool synthesizes values for these that ensure behaviour preservation.

Shrinkability and Robustness

Using shrinkability analysis, one can make sure that possible behaviours of the system are still present under perturbations. For instance, if clocks are used to model lower and upper bounds (say by l <= x <= u) on possible waiting times, shrinking means to forbid that the system acts on the boundaries of this interval. Thus, shrinkability analysis can complement the analysis by guard enlargement of [DDR05,DDMR08], and make sure that the model is robust to slight removal of behaviour. For example, this can help detect timing anomalies in scheduling, see [BMS12]. See here for an explanation of a timed automaton that is not shrinkable.

Moreover, following the same idea, one can actually use timed automata with shrunk guards to derive an implementation with imprecise clocks. In fact, the behaviour of a shrunk automaton under bounded guard enlargement is included in that of the initial automaton. Shrinkability is then a sufficient condition for the implementability of a timed automaton model. This approach is detailed in [SBM14].

Download

The tool is available for Linux. Although not tested, it should also work on Windows with Cygwin.

Source code and binaries (Linux i386): shrinktech-1.0.tar.gz


For a better experience, we recommend you to install Kronos.

Getting Started

A simple example

User guide

Case Studies

The column sim-graph shows the number of states and the number of transitions of the finite automaton F w.r.t. which the shrinkability is checked. An asterisk indicates bounded shrinkability, where only a portion of the time-abstract bisimulation graph was shown to be simulated by the shrunk automaton.


Modelstatestransclocks sim-graphtimeshrinkable
Lip-Sync Prot. (Exact)23068054000/8350* (subgraph)9sNo
Lip-Sync Prot. (Interval)2306805501/1282* (subgraph)9sYes*
Lip-Sync Prot. (Interval)23068054484/48049* (subgraph)28sNo
Phone Prot.1116563/2710.3sNo
Philips Audio Prot.44620972437/273446sYes
Root Contention Prot.651386500/3455* (subgraph)7sNo
Train Gate Controller6819911952/854034sNo
Fischer’s Protocol 31524643472/432120sYes
Fischer’s Protocol 4752286444382/65821310minYes
Fischer’s Protocol 5355216192510000/10000* (trace)42sYes*
And-Or Circuit1220480/4971.3sYes
Flip-Flop Circuit2234530/640.9sYes
Latch Circuit (Interval)32777105/3641.6sYes
Latch Circuit (Exact)32777100/3310.6sNo

The models can be found in the examples directory of the tool archive. They can also be downloaded separately here. The references for the models can be found inside.

Author

Ocan Sankur

References

[SBM14] Ocan Sankur, Patricia Bouyer, Nicolas Markey. Shrinking timed automata In Information and Computation 234, pages 107 - 132. 2014.

[San13] Ocan Sankur. Shrinktech: A Tool for the Robustness Analysis of Timed Automata In CAV'13 LNCS 8044, pages 1006-1012. Springer, 2013.

[SBM11] O. Sankur, P. Bouyer, N. Markey. Shrinking Timed Automata. FSTTCS 2011.

[BMS12] P. Bouyer, N. Markey, O. Sankur. Robust reachability in timed automata: A game-based approach. ICALP 2012.

[DDR05] M. de Wulf, L. Doyen, J.-F. Raskin. Almost ASAP semantics: From timed models to timed implementations. FAC, 17(3):319-341, 2005

[DDMR08] M. de Wulf, L. Doyen, N. Markey, J.-F. Raskin. Robust safety of timed automata. FMSD, 33(1-3):45-84, 2008.

À propos du LSV