TReX: A Tool for Reachability Analysis of Complex Systems

Aurore Annichini, Ahmed Bouajjani, and Mihaela Sighireanu

To appear at 13th Conference on Computer-Aided Verification (CAV01), Paris, France, 18-22 July 2001


Abstract

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.


Server START Conference Manager
Update Time 28 Mar 2001 at 08:36:01
Maintainer www-cav01@lsv.ens-cachan.fr.
Start Conference Manager
Conference Systems