Research On Fully Parallel Approach Of Model Checking Via Probe Machine

Model checking is an automated system verification technique through formal modelling of the system and formal descriptions of its properties,which uses search algorithms to determine whether a system satisfies the properties to be verified and gives reachable or counterexample paths.However,the state space can be extremely large for many practical systems,where the time and resources required for verification will grow exponentially with the number of states.It is the state explosion problem of model checking,leading to long and inefficient detection times,which limits the development of model checking in industry.To solve these problems,this paper proposes an approach of model checking based on probe machine,which achieves fully parallel system verification.The method takes the advantages of the full parallelism of the probe machine model to greatly reduce the time of graph search algorithms in model checking,and overcome the challenge that it's unable to handle state explosion through Turing machine.This paper applies the mathematical model of probe machine to the model checking problem,constructs a mapping relationship between them,and proposes a parallel verification method for LTL and CTL model checking,which expands the scale of system verification and improves checking efficiency.The MC2 PROBE model checker is also developed and applied to the vulnerability mining system,which improve the ablility of complex vulnerabilities detection in large-scale programs.In conclusion,the contributions are as follows:(1)A model checking mapping algorithm based on CTL semantics is proposed,which translates the Kripke structure into data library and probe library that can be run on existing probe machines.The method finds all counterexamples in the system with a single graph search,reducing the verification time against large state space systems.(2)An approach to find multiple accepting cycles in linear time is proposed,and a probe machine-based method for solving the strongly connected component is designed,which can reduce the verification time of CTL operator EG and LTL model checking.(3)A model checker called MC2 PROBE is developed to simulate the probe operation,which takes the system model as input and ultimately allows all feasible paths or counterexamples to be obtained.A number of simulation experiments are completed on various systems with different number of states.The results demonstrate the ablility of our approach compared to a conventional model checker.(4)A vulnerability detection system based on MC2 PROBE has been designed and constructed.It uses tools to disassemble binary code,through static analysis methods,which can automatically detect dangerous function call vulnerabilities and circular read/write vulnerabilities.This system combines the features of the MC2 PROBE model checker to solve the problems of poor search coverage,long search time and low search efficiency of traditional static analysis methods.