TREX

TREX

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

TREX can perform several functions including:

• Generation of the set of reachable configurations for the input model. For this, TREX uses symbolic reachability analysis on symbolic representation structures for representation of infinite sets of configurations.
• On-the-fly check of safety properties on the transitions of the input model.
• Check of some kind of liveness properties of the input model.

The general picture of the TREX environment is given below:

VO Integration: No

Active: No

Available Benchmarks: No

Website: https://www.irif.fr/~sighirea/trex/

Download: Link.

Documentation: Manual provided with distribution in UNIX man format. Also see these references and examples.

Contact: Aurore Collomb-Annichini, Ahmed Bouajjani, Mihaela Sighireanu

Excerpt and graphics from: https://www.irif.fr/~sighirea/trex/