An Efficient Generation of the Timed Reachability Graph for the Analysis of Real-Time Systems

As computers become ubiquitous, they are increasingly used in safety critical environments. Since many safety critical applications are real-time systems, automated analysis technique of real-time properties is desirable. Most widely used automated analysis techniques are based on state space exploration. Automatic analysis techniques based on state space exploration suffer from the state space explosion problem. In particular, a real-time system may have an unbounded number of states due to infinitely many possible time values. This paper presents our approach for generating a finite and efficient representation of the reachable states called a timed reachability graph for a real-time system. In this paper, a real-time system is specified using a timed automaton which is a timed extension of the well-known finite automaton. Our approach for coping with the state explosion problem is to extract timing information from states and to represent it as relative time relations between transitions. We also present an algorithm for computing the minimum and maximum time bounds between executions of two actions from a timed reachability graph to determine timing properties