A Complete Axiomatization For Propositional Projection Temporal Logic And Formal Verifications

As a mainstream technology of formal verification, theorem proving has been used toverify software and hardware with success. Being different with model checking, theoremproving has no relation to states and does not suffer from the state explosion problem. It canbe used to verify finite systems, infinite systems and parameterized systems. In the approachof theorem proving, first, both the system and desired property are specified into logical for-mulas; second, the proof of the system formula implying the property formula is constructedby using the axioms and inference rules, by which way the system satisfying the propertyis verified. This thesis investigates the methodology for formal verification using theoremproving based on Propositional Projection Temporal Logic(PPTL). PPTL is an extension ofPITL including new projection operator prj, projection-plus operator prj⊕, and infiniteintervals. PPTL is decidable as well as has a full ω regular expressiveness. It can be used todescribe sequential behavior, parallel behavior, iteration and selective construct in concurrentprograms. For taking advantages of these features, a complete proof system for PPTL hasbeen proposed. It consists of a set of axioms and inference rules which express the semanticsof operators in PPTL. The proof system is demonstrated to be sound by proving that all theaxioms are valid and all the inference rules preserve validity in the model theory of PPTL.The proof system is also proved to be complete whose proof is significantly based on theconcept of PPTL normal form. To reduce the proofs of some complicated case studies, somefrequently used theorems are proved in advance. In addition, a mutual exclusion problem isverified to illustrate the proof system is workable.The methodology for specification and verification of real-time systems based on PPTLis investigated. We take the famous Deadline Driven Scheduler as an example to illustratehow to program using MSVL, how to transform the MSVL program into a PPTL formula,how to specify the desired property, and how to verify the program satisfying the property. Inthe verification, many lemmas are involved and their proofs are not so straightforward that anon-trivial effort is required.The methodology for specification and verification of hardware system based on PPTLis also studied. A full adder and a carry lookahead adder are selected to illustrate the specifi-cation and verification process.With the development of many-core processors, the specification, development and ver-ification of many-core parallel programs become a grand challenge. To be able to specify theautonomy, concurrency and communication among different processes over a many-core pro-cessor, a new semantic model named Cylinder Computation Model (CCM) is proposed based on PTL. In CCM, a fine-grain interval is taken to be a communal time axis which is surround-ed by a cylinder of many coarse-grain intervals. The programs to be interpreted over thesecoarse-grain intervals can be viewed as the processes running over different cores on the samechip. These processes communicate over the common projected states. Thus, many-core par-allel computing can be modeled by CCM. Its syntax and semantics are defined based on thatof sequence expressions. Moreover, the arithmetic laws for sequence expressions and logicallaws for CCM are also presented. This is to establish the model theory of CCM. To realizethe specification of many-core parallel programs using CCM constructs, we incorporate CCMinto MSVL. First, the operational semantics of CCM is established based on that of MSVL.Second, the reduced algorithms for CCM operators are formalized in terms of the operationalsemantics of CCM. Finally, a word processor is specified using CCM.