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
-
treat.tar.Z
contains a Sun OS 5.5 (Solaris 2.5) compiled version of the TREAT system,
a user's guide draft, and and several examples.
- user's guide: PS file -
PDF file
Related Papers
- TREAT: Timed REachability Analysis Tool.
Inhye Kang, Insup Lee, Young-Jun Kim, Eugenia Ho, and
Young Si Kim,
submitted to
IEEE High-Assurance Systems Engineering Workshop, Aug 1997.
Abstract -
PS file -
PDF file
- A State Minimization Technique for Timed Automata.
Inhye Kang, Insup Lee, and Yong Si Kim,
Infinity Workshop, Aug 1996.
Abstract -
PS file -
PS file
- An Efficient State Space Generation for Analysis of Real-Time Systems.
Inhye Kang and Insup Lee,
International Symposium on Software Testing and Analysis, Jan 1996.
Abstract -
PS file -
PDF file
- State Minimization for Concurrent System Analysis
Based on State Space Exploration.
Inhye Kang and Insup Lee,
Proc. Conference On Computer Assurance, June 1994.
Abstract -
PS file -
PDF file
Please contact Inhye Kang (kang@saul.cis.upenn.edu) for questions
and comments about TREAT.
Last modified: March 10, 1997.