TReX: A Tool for Reachability Analysis of CompleX Systems

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 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 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. Proceedings of CAV 2001. (C) Springer-Verlag.
  • 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.
    • 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.
  • 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.
  • Liveness analysis for parameterized timed and counter automata:
    • A. Bouajjani, A. Collomb-Annichini, Y. Lacknech, and M. Sighireanu. Analysis of Fair Extended Automata. Proceedings of SAS'01, (C) Springer-Verlag.
  • Case studies:
    • A. Collomb-Annichini and M. Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. RTSS'01.
    • 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. 

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 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 .


 The following computer architecture 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 . Last modified: November 25, 2003