Projection temporal logic (PTL) is an extension of the first order interval temporal logic (ITL) by introducing a new temporal operator prj and supporting both finite and infinite time. Further, PTL has an expressive power of full regular expression and can conveniently express the program structures such as sequence, choice, iteration, parallel, semaphore, etc., which enables us to specify the implementation and property of the system to be verified within a unified PTL framework. The PTL based formal method can be employed to verify all kinds of hardware and software systems.To verify the properties of concurrent and reactive systems based on the theorem proving approach, this thesis investigates a complete axiomatization over finite domains for PTL. To this end, the techniques of normal form (NF), normal form graph (NFG), labeled normal form (LNF) and labeled normal form graph (LNFG) of PTL are intro-duced. Moreover, the decision procedures and the completeness proofs of the axiomatic system of PTL with finite and infinite time are given respectively based on the proper-ties that the NFG and LNFG can describe the models of PTL formulas, which makes a solid theoretical foundation for formal verification with PTL.The main contributions of the thesis are as follows:(1) An axiomatic system supporting both finite and infinite time is formalized for PTL. Further, the axiomatization allows temporal terms (terms with temporal opera-tors), functions and predicates, which to the best of our knowledge is the first time for an axiomatization of a first order temporal logic equipped with such items. Moreover, a lot of commonly used theorems and derived inference rules are proved based on the axiomatic system of PTL.(2) The techniques of NF and NFG are introduced, based on which the decision procedure is formalized and the completeness of the axiomatic system is proved for PTL with finite time. Firstly, the NF and the existence of the NF of PTL are defined and proved respectively. Further, the algorithm to compute the NF for PTL formula is presented. Moreover, the NFG of PTL is defined and the algorithm for constructing the NFG is formalized based on the NF of PTL. Finally, a decision procedure and the completeness proof of the axiomatization of PTL with finite time are given based on the properties that the NFG can describe the models of PTL formula.(3) The techniques of LNF and LNFG are introduced, based on which the decision procedure is formalized the completeness of the axiomatic system is proved for PTL with infinite time. Firstly, the definition of LNF and the algorithm to compute LNF is given. Further, the LNFG of PTL is defined and the algorithm for constructing the LNFG is formalized based on the LNF of PTL. Moreover, a decision procedure of quantifier free PTL (QFPTL) formula is presented based on the properties that the LNFG can describe the finite and infinite models of PTL formula. In addition, a generalized labeled normal form (GLNF) and generalized normal form graph (GLNFG) are introduced to transform any quantified PTL formula into its equivalent QFPTL formula. Thus, the decision procedure for any PTL formula with infinite time is obtained. Finally, the completeness of the axiomatization of PTL with infinite time is proved with decision procedure of PTL.(4) The key techniques of PTL based formal method are analyzed and an example is given to illustrate the effectiveness of the PTL based theorem proving approach in system verification for concurrent systems. Firstly, the expressive power of PTL is demonstrated by showing the equivalence between the full regular expression and the PTL formula. Further, the framed temporal logic programming language MSVL is employed to model the implementation of the system to be verified. Besides, a novel system modeling approach named Extended Kripke Structure is presented. Finally, as a case study, the process scheduler over multi-core CPU is modeled with PTL formula, and the correctness of the scheduler is proved with the theorem proving approach based on the axiomatic system of PTL. |