Research And Implementation Of Model Checking Algorithm Based On Grahp Theory

With the development of hardware productivity and software technology, the reliability and efficiency of hardware and software become more and more important.The higher requirement cause more cost. The traditional verification methods need too much manpower and material resources. In order to reduce the cost of production and development and ensure the reliability of its products, verification methods named formal verification based on mathematic are proposed and are widely used in industry.Recently, formal verification methods are researched based on many theorities.This thesis analyzes many existing methods and proposed a new formal verification method. The method models the system by adjacency matrix and uses CTL formula to represent the specifications which need to be satisfied. The verification process is the calculation of adjacency matrix instead of the running verification.First, a method to model the system based on adjacency matrix is proposed. The method gets the adjacency matrix of the system according to the encoding of the states in the state diagram and the transfer relation between these states. Since the adjacency matrix is the same as the system, the properties of the system can be represented by the calculation of the matrix.The verification method improves the model checking process from labeling to calculation. Different matrix formulas are given to different CTL operators. The satisfiability of the system can be got by the calculation of matrix formulas according to the CTL properties.Finally, a formal verification tool based on our method is designed and realized.The performance and efficiency of our method and tool are illustrated by two practical cases(FIFO and PCI bus). Compared with formal verification tool NuSMV, our method gets better results.