Research On SAT-based Model Checking Of Combinational Systems

A compositional transition system is a general formalism for specifying sophisti-cated behaviors of concurrent and distributed systems. Thus it is of great importance tostudy the correctness guarantee techniques of these systems. Model checking is an im-portant method for verifying compositional transition systems. However, due to the state-explosion problem, the problem size it can handle is limited. SAT-based model checkingis one of the most successful techniques for alleviating the state-explosion problem. Ben-efit from the existing efcient SAT solvers, many complex problems can be verified bythis technique. However, the state-explosion problem remains. Although the problemsize it can handle has been greatly improved, it is still difcult to verify the real-worldsystem in the large scale.This dissertation studies the SAT-based model checking of combinational transitionsystems. Our goal is to improve the model checking algorithms for compositional tran-sition systems, and thus enlarge the problem size it can handle. According to the frame-work of SAT-based model checking, this dissertation proposed various efective methodsand techniques on state transition model, model checking algorithm, and SAT solving,respectively. Based on these techniques, a model checker for compositional transitionsystems, called Tsmart-Beagle, is developed. Tsmart-Beagle is used to verify several realproblems. The main contributions of this dissertation include four parts:1. This dissertation proposes the macro-transition for compositional transition sys-tems. It proposes to execute a macro-transition during each step, and for the transitionswithin a macro-transition, the true-concurrency semantics is employed. Based on thisidea, this dissertation proposes a macro-transition-based state transition model and anefcient encoding scheme to construct this model. Both theoretical analysis and exper-imental results show that this method can greatly reduce the times of invoking a SATsolver to verify the property and the verification complexity.2. This dissertation proposes three optimization strategies for the widely used tem-poral induction algorithm. Temporal induction converts the model checking problem intoa sequence of highly-related SAT problems. Two optimization strategies are proposedto reuse the intermediate results of solving the previous problems, including the clausereplication and reuse technique, and the search tree reuse technique. The third strategy is to employ the structure information of the system to refine the SAT decision order.Experimental results show the efectiveness of the three strategies.3. This dissertation presents a novel efcient SAT algorithm based on maxterm cov-ering. The satisfiability of a clause set is determined in terms of the number of relativemaxterms of the empty clause with respect to the clause set. A set of synergic heuristicstrategies are presented and elaborated. We conduct a number of experiments on k-SAT(k≥3) problems at the phase transition region. Experimental results on public bench-marks attest to the fact that, our enhanced algorithm runs faster than zChaf and MiniSATfor most of k-SAT instances.4. We developed a model checking tool Tsmart-Beagle. It integrates the macro-transition technique and the optimized temporal induction algorithm in its SAT-basedmodel checking engine. We apply Tsmart-Beagle to the verification of several real prob-lems, including MTP, DPU, GCS. Experimental results show that it runs much faster thanNuSMV on these problems.