Research On SAT Based Symbolic Model Checking

With the advances in computer technology, the designs of hardware and software become more and more complexity, and the complex designs tend to contain more and more design ?aws and errors. The traditional methods can not ?nd all the design errors in the system. However, the safety of the systems are very important, especially for safetycritical applications such as aerospace, defense and health care. Therefore, veri?cation technologies are urgently required in such ?elds.Model checking is a technique for automatically verifying correctness properties of?nite state systems which is proposed in 1980 s. After 30 years of development, model checking has been one of the most important technique in the ?eld of computer aided veri?cation. However, this technique it limited by the state explosion problem the number of states of the system is exponential in the number of state variables. Researchers in this ?eld developed different algorithms to cope with this problem; e.g., BDD based symbolic model checking, partial order reduction and CEGAR. In recent years, with the advance of SAT technologies, Biere et al. ?rst proposed the Bounded Model Checking technique. It has attracted extensive interest from both academia and industry because of its advantage in ?nding bugs compared to BDD based model checking. At present, SAT based model checking is still a hot topic in computer aided veri?cation ?eld.However, in practice, there are still many problems with SAT based model checking,such as e?ciency, ability, completeness. In this thesis, we focus on how to improve the e?ciency, ability and completeness of SAT based model checking. The contributions of this thesis are listed as follows.1) We optimize the LTL bounded model checking technique to improve the e?ciency of bounded model checking for LTL.It consists of two optimization techniques. We name the ?rst technique as ”CounterexamplePresering Reduction(C?PR?. for short)”. The main idea of C?PR? is to reduce the input LTL formula into an ”equivalent” formula which is an easier-to-handle one before model checking with a light-weight technique. Hence, the reduced formula will replace the original formula in model checking. The technique is very e?cient in model checking,especially for complex formulae. We propose a new encoding technique in the the second optimization technique which makes use of the incremental SAT technologies. These two optimization techniques can be used together to improve the LTL bounded model checking. Experimental results show that, the new encoding is very e?cient compared to other encodings.2) We propose bounded model checking techniques for ω-regular property.LTL is not powerful enough to express all the ω-regular properties used in industrial veri?cation. Hence, it is very important to development bounded model checking for ω-regular properties. In this thesis, we propose three encodings for bounded model checking two temporal logics which can express all ω-regular properties. We propose the semantic based encoding for bounded model checking ETLl+f. The key part of the technique is to construct tableau for ETLl+f. We extend the LTL tableau construction technique to construct tableau for ETLl+f. We propose two encodings for bounded model checking QTL. The ?rst encoding is based on the syntax of QTL which we name as syntax based bounded model checking. The key part of syntax based bounded model checking is to encode the bounded model checking problem of QTL into an QBF formula which can be solved by an QBF solver. The other encoding technique is also an semantic based encoding. We achieve the tableau of QTL by extending the LTL tableau construction technique. The semantic encoding convert the model checking problem into an constraint fair cycle detection problem which can be encoding into an boolean formula that can be solved by an SAT solver.3) We present a complete SAT based model checking technique.Bounded model checking technique is not a complete technique, it can not prove properties. However, the model checking problem of linear temporal logics can be converted into a fair cycle detection problem, and the fair cycle detection problem can be handled by solving some reachability problems. Thus, the key part of a complete SAT based model checking algorithm for linear temporal logics is e?cient reachability algorithms. In this thesis, we propose two e?cient reachability algorithms. Both of them are based on Property Directed Reachability(PDR, for short). The intuitive idea behind these two algorithms is to approximate the reachable state space by bidirectional PDR.Experimental results has demonstrated its e?ciency.4) We have implemented two available tools.We implement the C?PR? technique, the incremental semantic based encoding for LTL and ETLl+f bounded model checking algorithm in ENu SMV which is an extension of Nu SMV. An reachability analysis tool, namely Reach is also designed and implemented. It also supports interleaving PDR algorithm and parallel PDR algorithm presents in this thesis. Except that, the tool also supports many other algorithms, such as BMC,k-induction based model checking, interpolation based model checking and basic PDR algorithm.