TREAT: Timed REachability Analysus Tool

Real-Time Systems Group

The University of Pennsylvania

TREAT: Timed REachability Analysis Tool

TREAT is a tool for generating timed reachability graphs (TRGs) for CTSM using state minimization algorithms for data state space and timed state space. The input is a textual representation of a CTSM system which consists of a set of processes. TREAT has a parser and a TRG generator. The parser translates the textual input to a program in C++ which defines an internal data structures for the CTSM and includes function calls for CTSM process composition and TRG generation. The TRG is a textual form, from which users analyze the correctness. We are currently developing the graphical interface in Tcl/Tk for TREAT.

Obtaining TREAT

Related Papers

Please contact Inhye Kang ( for questions and comments about TREAT.

Last modified: March 10, 1997.