Timed Automata Up Study

Model checking is a formal method used to verify safety and correctness of real-time systems. As the computer science advances, the method of model checking has been broadly accepted and utilized. But the bottleneck is the state space explosion problem when constructing systems by model checking method. The key of model checking is the minimization of the state space. Specification and verification of real-time system based on timed automata consist of constructing its timed automata and verifying its property. Namely the key is minimization of state space and reachability analysis. We focus on it in this paper.Because most property to be verified are simple and can be verified without constructing the whole state space, we focus on the problem of reachability. In this paper, we research on the problem of reachability of timed automata and analysis the different methods of determinant of reachability. Our work emphasizes the analysis of determinant of reachability based on clock constraints. This paper presents representation of clock constraints and a method of computing succession basing on reachability analysis of clock constraints, the method can minimize the state space of succession and reduce the problem scale. We also present the pretreatmentmethod of reachability analysis algorithm, which can reduce the memory usage and improve efficiency of the algorithm.