TReX: A Tool for Reachability Analysis of Complex Systems

The paper describe a tool, called TReX, allowing to analyse automatically automata-based models equipped with variables of different kinds of infinitedomain data structures and with parameters (i.e., uninstantiated constants). These models are, at the present time, parametric (continuous-time) timed automata, extended with integer counters and communicating through unbounded lossy FIFO queues. The techniques used in TReX are based on symbolic reachability analysis. Symbolic representation structures are used to represent infinite sets of configurations, and forward/backward exploration procedures are used to generate a symbolic reachability graph. 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