Verification Techniques Based On Timed Automata Model

With the development of computer science, industry is increasing emphasis on the accuracy and reliability of the system. Formal model validation has been widely used. Through the reachability analysis, model checking real-time systems can complete the safety and activity of verification. Its idea is to search for system behavior described in the conversion system, and then analyze the state set up in order to determine whether the system to meet the specification. Timed automata(TA) is a time-constrained system of finite-state conversion. It is the most widely used method of formal verification.Part in theoretical studies, first of all an analysis of the concept of timed automata, and then given a number of TA extended form. Real-time system events can occur in the corresponding TA with a state to start from the initial state can reach, therefore the main task of model validation is a state reachability analysis. State is described by some symbolic way in the validation. we analy the clock region and clock zone, the two main methods of reachability analysis are give at last. We are focused on the binary decision diagram based on the model validation methods, and it is premised on the use of automated machines in time integer Semantics。we explain how the configuration sets and transitions of this integer semantics can be represented as BDDs. We give the reachability analysis algorithm improvements with this data structure, then analyze the complexity of the algorithm with a concrete example of the verification, show that for some models the reachability analysis seems to be of polynomial time and apace complexity.Part in applied research, first of all introduced tool uppaal based TA, and then given model validation'steps and modeling standards.In addition,at last structured TA models of the aircraft landing control system and the elevator control system,and verify their property,so errors can be avoided in the system actual running. Through the use of uppaal verification tools, we can easily construct models for the system, which will help designers to understand the operation of the system process, the timely detection of some of the problems that exist in the system.