Optimization Of Model Verification Methods Based On Timed Automata

Real-time systems is a kind of systems with time constraint. The action is connected with some time constraint. Correctness and security are important to these systems, so analysis and validation are needed. The validation of real-time systems not only needs the logic is correct, but also the time is correct. The protocol complexity is increasing rapidly, every fault is harmful to the stability and the reliability. The validation of protocols also needs to validate some property of time.Finite automata is an important technique of formalized description and validation. It is the foundation of many formalized techniques.. It can be assembled with other techniques. But it doesn't have clear concept of time. So it can only deal with the sequence of events and can't describe the time clearly. R.Alur has put a theory of timed automata . Timed automata included time variables into finite automata.The state-space of timed automata grows exponentially with the scale of questions . The validation of systems based on timed automat becomes very complex when the scale of questions is large. So the optimization of the technique of model checking based on timed automata is needed.In this paper , we research region automata, zone automata and the method of state space minimization based on history equivalence and bisimulation transition. We develop a symbolic method of the presentation and computation of regions. So it is easier to use the regions. We develop a method based on the time relation of transitions. This method computes the earliest time and the last time of transitions to decide the transitions are valid or not. Then the minimized transition systems can be get through getting rid of the transitions which are invalid.A lot of automatic tools have been developed on timed automata. These tools have been use widely during the validation of real-time systems and protocols. In this paper, we check the FDDI protocol using Kronos .