Based On Timed Automata Model Verification Theory And Applied Research

Real-time systems are usually used in safety-critical environment, which are important computer application systems. It is extremely important to ensure the correctness of these systems. So it is necessary to specify and verify the properties of real-time systems using formal methods.Based on timed automata developed by R. Alur, theories of specification and verification of real-time systems and their applications are described in this paper. Real-time systems are specified and verified by checking whether the intersection is empty, which is the intersection of timed regular languages received by automaton models of system with the languages received by its specification automaton models. The common methods are constructing region automata and zone automata. When the scale of a system is very large, it is difficult to specify and model it, what's more, the problem of state-space explosion may occur as well. Then it is in great need of the formal technique of automatic verification to solve these problems.UPPAAL is a kind of automatic verification tool, which takes the timed automata as its behavioral model and plays a very important role in the specification and verification of real-time systems and communication protocols. To resolve the problem of state-space explosion, UPPAAL uses constraint solving techniques and forward verification techniques to avoid building the state space that are not reachable. However, the system can not deal with problems in an efficient way, for the absence of heuristic information and the presence of some useless state circles. Thus an improved algorithm utilizing heuristic information is proposed to settle these problems mentioned above. In the algorithm, an evaluation function is designed to evaluate the cost of reaching aiming global state for every global state; and the useless state circle is defined to avoid analyzing useless states repeatedly. In the following sections, a communication protocol is analyzed and specified, followed by the automatic verification of the timed automaton models of this protocol based on UPPAAL, which proves the correctness and safety of the protocol.As a type of model-checking tools, Petri Nets extended with time factors are suitable to describe and analyze real-time systems. But they can only offer limited analysis capabilities sometimes. A translation algorithm is described in this paper, which can map a timed Petri nets model of a railroad crossing system with a single controller platform into a set of semantically equivalent timed automata. Then the properties of safety and bounded liveness of the transformed system is verified by UPPAAL.