TReX: A Tool
for Reachability Analysis of CompleX Systems
[Introduction
| References | Examples | Download
| Manual | Team
]
Introduction
TREX is a tool for
automatic analysis of automata-based models equipped with variables belonging
to different infinite/finite domains and with parameters. These
models are, at the present time, parametric (continuous-time) timed automata,
extended with integer counters and finite-domain variables, and communicating
through unbounded lossy FIFO channels and shared variables. This model is
a subset of the model taken in high-level languages like SDL.
At the present time, TREX
does:
- Generation of the set of reachable configurations for the input
model. For this, TREX
uses symbolic reachability analysis on symbolic representation
structures (see references [1], [2])
for representation of infinite sets of configurations. The exploration of
reachable configurations can be done forward or backward. The termination
is not guaranteed, but efficient extrapolation techniques (see
references [1], [2]) are used to
help it. These techniques are based on computing the (exact) effect of the
iteration of control loops detected dynamically during the search.
When the analysis terminates, TREX
generates an abstraction of the input model given by a set of reachable
configurations and a finite symbolic graph. The set of reachable configurations
can be used as an invariant of the system (synthesis of constraints).
For instance, if the analyzed infinite-state model M is already an
abstraction of a more concrete one M', the set of reachable configurations
of M can be used to construct an invariant of M' which may
help in its analysis. On the other hand, the generated finite symbolic graph
is a finite abstraction of the analyzed model, which can be used for finite-state
model checking. - On-the-fly check of safety properties on the
transitions of the input model. The property should be given as an observer,
i.e. an extended automaton sharing transition labels with the input model.
If the property is not satisfied, TREX generates a diagnosis showing the sequence of
transitions from the initial state of the model to the state firing the
bad transition. The symbolic configuration of the fail-state can be used
to synthesize constraints under which the safety property is satisfied.
- Check of some kind of liveness properties of the input model.
TREX can synthesize
fairness constraints stating about the bounded iterability of some kind of
loops (see reference [3]).
The general picture of the TREX
environment is given below:
The input model of TREX
is given by a textual IF
file. This file can be obtained by translation (using IF tools) of a graphical
SDL specification, or of a textual LOTOS one. Also, the IF file can be used
to do, after instantiation of parameters, finite model-checking with the CADP or KRONOS. The input
model is the only mandatory input of TREX.
Additionally, the user can specify initial constraints on the parameters
occurring in the model. These constraints play the role of an invariant:
they are true in each reachable configuration explored by TREX. The exploration can
begin either from the initial state of the model or from a symbolic initial
configuration specified by the user.
The core of TREX are
a forward/backward exploration algorithm and the symbolic representation
structures for infinite sets of valuations for variables. The exploration
algorithm is generic and can be used for any kind of data structures
for which it is possible to provide a symbolic representation structure,
a symbolic successor/predecessor function, and an extrapolation procedure.
In the current version, TREX
provides three packages for symbolic representation of configurations:
- SRE (Simple Regular Expressions) [1] package for
lossy FIFO channels,
- Constrained Parametric DBMs [2] for parametric
timed automata and counter automata, and
- FOAF (First Order Arithmetical Formulas) [4]
for linear and nonlinear constraints on parameters.
The finite graph generated by TREX
is in ALDEBARAN format, one of the graph formats of CADP toolbox. Using CADP, the
graph can be minimized using different equivalence relations implemented in
ALDEBARAN tool or it can be model-checked using XTL tool.
The symbolic reachable configurations generated by TREX can be used inside abstraction
tools like InVest.
Related publications
- TREX has been
presented for the first time at CAV'01:
- A. Annichini, A. Bouajjani, and M.Sighireanu.
TreX: A Tool for Reachability Analysis of Complex Systems.
To appear in Proceedings of CAV 2001. (C) Springer-Verlag. [ps]
- Presentation of data structures (SRE) and algorithms for systems
with lossy FIFO channels:
- P.A. Abdulla, A. Bouajjani, and B. Jonsson. On-the-Fly
Analysis of Systems with Unbounded, Lossy, FIFO Channels. Proceedings
of CAV'98, (C) Springer-Verlag, volume 1427 of LNCS, pages 305-317. [ps]
- P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic Verification
of Lossy Channel Systems: Application to the Bounded Retransmission Protocol.
Proceedings of TACAS'99, (C) Springer-Verlag, volume 1579 of LNCS. [ps]
- Presentation of data structures (Constrained Parametric DBM) and
algorithms for parameterized timed and counter automata:
- A. Annichini, E. Asarin, and A. Bouajjani. Symbolic
Techniques for Parametric Reasoning about Counter and Clock Systems.
Proceedings of CAV 2000, (C) Springer-Verlag, volume 1855 of LNCS, pages
419-434. [ps]
- Liveness analysis for parameterized timed and counter automata:
- A. Bouajjani, A. Collomb-Annichini, Y. Lacknech,
and M. Sighireanu. Analysis of Fair Extended Automata. To appear in
Proceedings of SAS'01, (C) Springer-Verlag. [ps]
- Case studies:
- A. Collomb-Annichini and M. Sighireanu. Parameterized
Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX
Submitted June 2001. [ps]
- P. Abdulla, A. Annichini, and A. Bouajjani. Symbolic Verification
of Lossy Channel Systems: Application to the Bounded Retransmission Protocol.
Proceedings of TACAS'99, (C) Springer-Verlag, volume 1579 of LNCS.
[ps]
TREX examples
For each example, we give an informal description, the formal description
using extended automata, the set of reachable configurations and/or the
finite graph obtained with TREX.
You can find here
the format used for description of input model of TREX.
Download TREX
The stable version of TREX
is version 1.3 released February, 14, 2003. A test version 1.4 is available on demand. TREX is entirely developed
in C++.
You can find an history of TREX versions
here.
The following computer architectures and operating systems are currently
supported by TREX.1.0
:
- "sun5": Sparc stations running SunOS 2.5, 2.6, 7 or higher
- "iX86": PC computers running Linux 2.0 (libc6 binaries)
In order to download TREX,
please follow the following steps:
Release notes for TREX
- TREX uses decision
procedures for integers and reals implemented in Omega and Reduce tools. Although the
use of Reduce may be avoided by the use of decision procedures implemented
in TREX (option -e),
the use of Omega cannot be avoided.
- IF language,
which is the language used in input of TREX for the description of extended automata, does
not yet support the specification of parameters. For this reason, the IF parser raises warnings
and errors concerning the parameters. These warnings are not relevant for
TREX, and should be
ignored.
Download FOAF
Inside TREX distribution you find
also the FOAF library (libfoafmodel.a).
FOAF is a library for representation and simplification
of non-linear formulas over real and integer variables. For linear formulas
on real variables, FOAF also provides an implementation
of parameterized Fourier-Motzkin procedure for quantifier elimination. Here is a C++ file describing the use of this library.
Download old version of TREX
You can download here
TREX in version 1.0 released January,10,
2001.
Manual
For the moment, the only manual provided for TREX is given within the distribution, in a Unix man
format.
TREX people
Please send questions or comments about TREX here.
A mirror site is maintained at Verimag.
Last modified: November 25, 2003