Research On Timed Automata And Its Application

Real-time systems have been widely applied in military and civilian fields. How to ensure the safety and reliability of such systems is widely concerned by researchers. The method of model checking is a formal verification method that analyzes and verifies real-time systems. Timed automata is an effective tool for the verification of model checking. It is the expansion of automata theory, provides formal method to establish and analyze the behavior of real-time systems. Timed automata is an important application in model checking, and has become the research focus of computer science theory.Zone automata is the finite construction of classical timed automata. Its state is a pair composed by clock zone and state, so how to represent and operate clock zone is the key realizing zone automata. There have been several effective representations in practice, such as DBM, CDD, etc. DBM is the data structure widely used. This paper researches timed automata theory, the representation and fomalization of clock zone. The main works are as follows:Firstly, this paper analyzes timed automata theory and related properties systematically, introduces region automata and zone automata.Secondly, by the analysis of the DBM representations, this paper sorts out a class of clock zone. In view of this kind of clock zone, an algorithm is presented for "normalization" of DBM, which improves time performance compared to the classical "floyd" algorithm. Based on this characteristic, the storage space also can be compressed. Theoretical and experimental results show the effectiveness of this method.Finally, a control system of railway intersection is modeled, the safety and reliability are verified.