The Formal Verification Techniques For The Timed System Using Timed Automata

The formal verification of timed system is more difficult than that of the general system because of introducing the timed domain. The researches on this subject attract many computer scientists in industry and university. An integrated formal verification framework FVofTA (Formal Verification of Timed Automata) is designed and developed using the theorem prover PVS (Prototype Verification System) in this dissertation for the purpose of modeling and verifying the timed system. On the basis of the timed automata theory, FVofTA is free of state space explosion because the modeling implementations are in PVS specification language and the verification process are carried out using PVS proof checker. The main contributions of this dissertation include the following parts:(1) As the basis, the manipulations of the clock/time are formalized using PVS specification language because time is one of the necessary elements in modeling the timed system using timed automata. In the meantime, some common clock operations for simplifying the modeling process are generalized and formatted.(2) The syntax and the semantics of the timed automata are implemented in PVS specification language. As the preparation of the formal verification, many lemmas, which assert some properties about the behavior of the timed automata, are also formalized and proved.(3) A template for modeling a general timed system is generalized according to the features of the timed automata syntax. Based on the manipulations of the timed automata, another template for the product construction is also acquired based on the communications among several timed automata. Using the two templates, a timed system can be modeled conveniently and efficiently.(4) Some formal theories about timed branch (linear) temporal logic were established over the states (runs) of the timed (Buchi) automata. This formalization can be used to describe both safety properties and bounded responses properties. A general interface is provided for describing the properties of timed system.(5) Based on the works in (2), a formal verification of the state invariance (also called safety property) in timed system is established using the lemmas about the runs of timed automata. The safety property can be deduced in a unified form because of the inductiveness over the runs of a timed automaton. (6) Some proof strategies are developed for the purpose of improving the verification process.(7) In order to investigate the whole state space, some model checking algorithms are integrated based on the region equivalence theories. This work can be used to detect deadlock in the timed behavior of a timed system. As a by-product, an error is uncovered in the region-equivalence definition by formalizing and proving the clock region equivalence which is extensively referred in many papers.(8) Three typical cases are investigated using the above methods and techniques. They are: 1) the automatic controller that opens and closes a gate at a railroad crossing, which satisfies safety and bounded response properties, 2) the Fischer protocol system that satisfies mutex property, 3) the biphase mark protocol system that is a convention for representing both a string of bits and clock edges in a square wave, which satisfies the correctness in sending and receiving a string of bits. It is shown that FVofTA can be qualified to modeling and verifying timed systems successfully from the fact that the satisfied verification results can be acquired.