Research On Symbolic Model-Checking Algorithms

Origins from 1980s', Model Checking is a kind of formal verification technology, whose birth is to overcome the limitation in the verification of finite-state concurrent systems by simulation and theorem proving technology. It is an automation technology for determining whether a finite system satisfies a given specification that has been successfully used in verifying the complex sequential circuit designs and communication protocols, and also achieves a lot in testing the reliability of software.The process of model checking consists of three steps: modeling the system by the Kripke structure, describing the desired property of the system using propositional temporal logic formula and verifying whether the Kripke structure satisfies the formula. Among this, Kripke structure is a four-tuple defining on a set of atomic propositions and is used to represent the states and the transition relation of the system; propositional temporal logic includes CTL*( computation tree logic) and its two sub-logic that is LTL (linear time temporal logic) and CTL (branching time temporal logic). Assumes that M is the Kripke structure of the system, s is the initial state for the system, while propositional temporal logic formula f describes the property which the system is going to meet, this article will focus on talking about model checking algorithms.Generally, there are two types of basic model checking algorithms: explicit model checking algorithms and symbolic model checking algorithms, and the former includes the Labelling algorithm and the Tableau algorithm. The Labelling algorithm which is used for CTL model checking is proceeding by labeling the state of M by the subformula of f which is true on it, and deal with each formula in turn from the min-subformula (true, false and atomics) to the outside by finally returning the set of states labeled by the formula f, at last we can determine whether M satisfies f by checking if the set contains the initial state s. The Tableau algorithm which is used for LTL model checking consists of three steps: first, it constructs a Tableau T?f for the path formula?f which contains all the paths that satisfy that path formula; and then combines M and T?f to generate a new Kripke structure M ' which contains all the paths that appear in both M and T?f ; at last tests whether there is a path from s in M ', if so then M doesn't satisfy the LTL formula Af and the path funded is the count-example to illustrate the conclusion, otherwise we can say M satisfy the LTL formula Af. The above explicit model checking algorithms use directed graphs or tables to represent the state space of the system, for the state space has an exponential increment with the system size, the time and space complexity is out of tolerance by using this algorithm to check complex system, this kind of state space explosion problem greatly limits the scope of its application.Symbolic model checking which is first proposed by McMillan is a technology of representing the state space of the system using symbolic method, the main idea of it is to use Boolean functions to express the set of states and the transition relation of the system, and then use OBDDs(Ordered Binary Decision Diagram) to store these functions in the computer with implementing the operations of them by OBDDs, it finally calculates the set of states that satisfy the given specification based on the fixed point theory in theμ-calculus. This technology usually operates on states set and transitions set rather than individual state and transition, for there is no direct relationship between the system size and the size of sets represented using OBDDs, it greatly alleviates the state space explosion problem, and has wide use in designing the system of large-scale integrated circuits with the ability of verifying systems over 10120 states.So far, there are symbolic model checking algorithms for CTL and LTL, but a number of the famous symbolic model checking tools don't support checking CTL* which is more expressive than CTL and LTL, even though some scholars have also given the symbolic method of the CTL* Model Checking, they didn't consider the fairness constraints. In this paper we propose an algorithm framework of symbolic model checking for CTL* with the ability to deal with fairness constraints, which includes the process of representing the system model by using OBDDs, the characterization of the temporal logic operator by fixed point theory and the symbolic algorithm of CTL* model checking.First, the states are coded with the labeling function of M which labels each state with the set of atomic popositions true in that state in order to express states set as Boolean functions; each of the transitions is related to a link of two states code correspondingly, so the transition relationship of the system can also be expressed by Boolean function. Then we can get the symbolic Kripke structure by generating the OBDDs of the Boolean functions which identify the entire states and transitions.Secondly, the power set of states set of M forms a complete lattice under the set inclusion ordering, each element of the lattice is called a predicate, and from the Knaster-Tarski theorem we can know that every monotonic predicate transformer defined on the lattice has a unique greatest and unique least fixed point. Each basic CTL operator can be defined as a monotonic predicate transformer on the lattice in order to have a fixed point characterization, although operator EX don't have a fixed point characterization, it can be expressed by a quantified boolean formula with nested existential quantifiers, for it is convenient to calculate the quantified boolean formula as well as greatest and least fixed point, we can get the symbolic model checking algorithm for CTL. The Tableau algorithm has given a method of converting the LTL model checking to a CTL model checking with fairness constrains, we can easily get the symbolic model checking algorithm for LTL by making the conversion symbolic and having a fixed point characterization for fairness constrains.At last, a decomposition theorem is proposed to deal with symbolic model checking problem for CTL* with fairness constraint, which converts the problem to symbolic model checking for LTL and CTL with fairness, the basic idea is to replace the max-replaced-subformula in the CTL* formula with states set which contains all the states that satisfy the subformula, the new formula after replacement can be checked by the symbol model checking algorithm for CTL and LTL, we continue to decompose the subformula until it is a CTL or LTL formula. Fairness constraint in CTL can be handled symbolic by using its fixed point characteration, while in LTL it can be integrated into the LTL formula to form a new LTL formula which can be checked by the symbolic model checking algorithm for LTL without fairness constraint. By dealing with fairness constraint in the symbolic model checking procedure for LTL and CTL, the algorithm framework proposed in this paper can symbolic model checking CTL* formula with fairness constraint. Based on the source code of open source model checker NuSMV, the framework is implemented and verified through some examples.