Study On Symbolic Model Checking Of Propositional Projection Temporal Logic And Its Applications

Model checking is an important formal method for the verification of hardware, software, multi-agent systems, communication protocols, embedded systems and so forth. Within the technique of model checking, the system under verification is modeled as a finite state machine, such as Kripke structure, state-transition structure and automata; while the desired property is expressed in a temporal logic formula. Then, model checking performs an exhaustive search procedure to automatically examine behaviors of the system and determine if the system in question conforms to the given specifications. Nevertheless, existing model checking approaches mostly rely on explicit representation and manipulation of the target state space, the size of systems can be verified is severely limited even when utilizing optimization techniques such as on-the-fly state space construction and partial-order reduction. In realistic designs, the size of the system model may grow exponentially with the number of concurrent components, constituting the main practical limitation of model checking. Moreover, existing formal specification languages, such as Computation Tree Logic (CTL) and Linear Temporal Logic (LTL) are limited in expressive power, such that sequential, concurrent and iterative properties are difficulty (or impossible) to be described by them. Motivated by this, in this dissertation, the methodology for symbolic model checking verification of Propositional Projection Temporal Logic (PPTL) properties and its applications are investigated in detail.As an extension of Propositional Interval Temporal Logic (PITL), PPTL introduces some new temporal operators and has been proved to have the expressiveness of full regular expressions. It can conveniently be applied to the specification of sequential, parallel, selective, state sensitive and periodic properties for concurrent systems. Symbolic model checking (SMC) is a useful and successful mechanism for ease the state space explosion problem easily encountered in explicit state model checking. The basic for symbolic model checking is representing the system model and the specification symbolically using boolean functions, and then searching the system model for those states which satisfy the specification with a traversal algorithm implemented on Reduced Ordered Binary Decision Diagrams (ROBDDs). For taking the advantages of both PPTL and symbolic model checking, a coherent framework for symbolic model checking verification of PPTL properties has been proposed. With this framework, the system to be verified is described by a Kripke structure M= (S,I, R, L), where S is a finite set of states,I(?) S is the set of initial states, R C S x S is the transition relation over state set S and L is the labeling function that labels each state with a set of atomic propositions true in that state; while the desired property of the system is expressed in a PPTL formula φ. Then, the complemented desired property -φ is transformed to its normal form. As normal form is the basis for constructing the labeled normal form graph (LNFG) which contains possible (finite or infinite) models of the corresponding formula, the set Sat((?)φ) of all state s ∈ S such that (?)φ holds on every path that begins at s can be figured out accordingly. In this way, whether the system model M satisfies the property φ or not can equivalently be checked by determining the emptiness of Sat((?)φ)∩I, i.e. the set of state s ∈I (?) S which satisfies (?)φ. Further, the complexity of the symbolic model checking verification of PPTL properties is analyzed. In fact, our model checking procedure runs in time O((log|V(φ)|)×|V(φ)|×(|R|+|S|)), where V(φ) denotes the set of nodes in the LNFG of the property formula φ, while |R|+|S| indicates the size of the system model M. In addition, cases about logic circuits or embedded systems are employed to show the feasibility of our model checking approach.The methodology for the verification of real-time and embedded computing systems using symbolic PPTL model checking is investigated. We take a task set scheduled with Rate Monotonic Scheduling (RMS) algorithm and Delayed Rate Monotonic Scheduling (DRMS) algorithm as examples to illustrate how behavior of real-time and embedded system can be modeled by Kripke structure, then represented by boolean functions and further manipulated with ROBDDs, how to specify the desired property of scheduling algorithm, and how to perform the formal verification of the system scheduled by RMS and DRMS satisfying the feasible specifications severally by means of symbolic PPTL model checking.Symbolic model checking for linear-time and branching-time temporal logics have been s-tudied extensively in the field of formal verification techniques over the past few years. As typical representatives of temporal logics, LTL and CTL are often applied to specify properties in symbolic model checking. Corresponding model checkers based on them, such as SMV, NuSMV and NuSMV2, have also been implemented. However, the above model checkers suffer from the expressive limitation of their formal specification languages. Extensions must be introduced into them for describing the sequential, parallel, selective, state sensitive and periodic properties. Moreover, these model checkers cannot be directly applied to PPTL spec-ifications. Consequently, symbolic model checking approach of PPTL is implemented within NuSMV to support the specification and verification of PPTL formulas. Moreover, formal operational semantics and symbolic model checking approach for Verilog programs are stud-ied based on symbolic PPTL model checker. Finally, cases about the verification of Gigamax cache coherence protocol, alternating bit protocol and PCI bus protocol are employed to illus-trate how symbolic model checker of PPTL works.