TREAT: Timed REachability Analysis Tool.
In-Hye Kang · 1999
This paper presents TREAT, a timed reachability analysis tool for the specification and analysis of a distributed, real-time system. Communicating Timed State Machine (CTSM) is a formal model for describing a system for TREAT. TREAT effectively constructs a finite, minimal labeled transition system which the user uses to analyze the correctness of a system described in CTSM. TREAT provides a graphical user interface as well as a text-based interface for user to describe a system in CTSM. 1 Introduction There has been significant progress in the development of formal methods for the design and automatic analysis of real-time systems in an effort to increase safety and reliability. One of the most prohibitive barriers in automatic analysis is state explosion. This problem is particularly serious in real-time systems because unbounded time values cause the state space to be infinite even for simple systems. Our research has focused on state space reduction for This research was suppor...