Bread First Search Based Model Checking

Model checking technology is a very important formal verification technology, andits biggest advantage is the automatic validation. Model checking technology has beenused in computer hardware, communication protocols, control systems, securityauthentication protocol analysis and verification, and achieved remarkable success, andradioed from academia to industry. However, the state space explosion problem inmodel checking process seriously restricts the application of model checkingtechnology in the industry.In this background, learning model checking technology related theoreticalknowledge, including temporal logic, automata and model checking algorithms. Aroundthe disk-based the BFS bread-first search model checking technology, analysis ofresearch focuses on the delay duplicate detection in the process of model checking,mainly as follows:1Research the delayed duplicate detection of state space searching of modelchecking process, and propose a method of partition-based delayed duplicate detection.The states of some of the layers for BFS breadth-first search can not be stored in thememory, and impact the conduct of the model checking. If the states of each layer aredivided, in order to adapt to memory restrictions, the model checking performance willbe improved.2Study the finite-state system state transition localized statistical properties, andpropose a method that applies the statistical properties to the partition-based delayedduplicate detection. The method reduces the number of states that need to be read fromthe disk in a disk-based delayed duplicate detection process, and also ensure that thestate-space search can be terminated, thereby improving the efficiency of the modelchecking.3On the basis of open software Murphy, implement the new BFS bread-firstsearch model checking tool of based on disk, and conducted comparative experiments.Experimental results show that the implementation of this article model checking toolsimprovint the time efficiency of8.37%.