Research And Implementation Of Model Checking Algorithm Based On Semi-tensor Product

With the rapid development of Computer Science, C loud computing, Io T and Mobile Internet has become a hot topic. Reliability is a challenge for the development of software. And the development of software is a challenge for hardware performance. In fact, it is a requirement of the proposed hardware performance. But the correctness and reliability of IC have always been a bottleneck during the hardware development. Simulation as a very popular method to verify systems can only find the errors. But simulation cannot prove the correctness of the systems because of its disadvantage. While software verification is immature, and there are not many methods. Therefore, verification is very meaningful for whether software or hardware.In this thesis, a new model checking algorithm is proposed based on semi- tensor product. The algorithm includes three parts: system modeling, property description and model verification algorithm.In order to model the verified systems, the atomic formulas are ordered according to the atomic sets of the systems. The Boolean values of the system states are defined according to the values of the atomic formulas under different system states. Then the system states are defined as vectors by the logical abstraction method based on semi-tensor product. The structure matrix is decided by the order of system states and adjacency matrix of the system model graph. Finally, the correctness and limitation of our model checking algorithm are proved by the vectors of the runtime systems.CTL(Computation Tree Logic) is used to describe the properties of the verified systems. CTL formulas are formulated according to the adequate sets of CTL connectives. The algorithms to verify EX, EG and EU are designed, using which the systems can be verified according to the semantics.At last, some case studies are given to show the system modeling, property description and model checking, which illustrate that our model checking algorithm not only can verify the software and hardware systems but also can be applied to other research fields.