We present a tool for automatic analysis of infinite-state systems
modeled by means of extended automata.
The models that can be analysed are parametric clocks and counters automata
communicating through lossy FIFO-channels.
The tool, called TREX, uses symbolic representations for infinite-state domains
(regular expressions, parametric DBMs, arithmetical constraints),
and forward/backward reachability analysis procedures,
enhanced with acceleration techniques in order to help termination.
TREX allows on-the-fly verification of safety properties, the generation of
the reachability set which can be used, e.g.,
for parameter synthesis and for invariant generation,
and the construction of a finite symbolic graph which can be used
for finite-model checking.
The tool is interfaced with the IF environment allowing
to use SDL as a specification language, and to interact
with abstraction tools and finite model-checkers.
