The Research And Implementation Of Parallelization Method For Program Verification

With the rapid development of computer technology,human life has become increasingly dependent on computer software.As software functions become more powerful,its complexity and integration level have increased dramatically.Consequently,disasters caused by software vulnerabilities have also occurred frequently.Especially,in some key areas,a software vulnerability may cause serious consequence.Therefore,the security and reliability of software need to be guaranteed.Program verification,as a verification technique for verifying the security and reliability of software systems,is dedicated to determining whether a system has correctly completed a preset goal.Currently,program verification has been widely applied to software securityrelated analysis and verification,and has achieved great success.As a code-level runtime verification tool,UMC4 MSVL,using Modeling Simulation and Verification Language(MSVL)program M to describing the system,Propositional Projection Temporal Logic(PPTL)formula P describing properties,dynamically executes the program containing system and property information to verify the validity of the property.The tool uses depthfirst search ideas for different branches of the program to verify it,after verifying a branch path,it traversing and verifying other branch paths.In order to further improve the efficiency of program verification,based on the hardware provided by multi-core computers,this paper introduces the idea of parallelization of program verification,achieves parallel verification of UMC4 MSVL,and validates multiple branch paths at the same time to improve program verification efficiency.The main contributions of this article are divided into the following points:1.Research on UMC4 MSVL validators,including verification principles,verification methods,and tool implementation,and propose the idea of parallel verification.2.Design a parallel verification framework for UMC4 MSVL and implement it.Implement the multi-threaded modules,package the depth-first search process into task and submitting them to the task queue,and perform multiple tasks at the same time using thread pool technology to verify multiple branch paths simultaneously.Solve the problem of mutual exclusion of variables in parallel verification.Implement parallel verification of the MSVL statements,and provide a solution for parallel verification of the MSVL parallelism statements.3.Implement the counterexample path output function.When the desired property is not satisfied,it can output the execution path that dissatisfy desired property,which is convenient for the verification user to analyze.4.Test the efficiency of parallelization verification by magic squre examples and wolfsheep-cabbage example,and test the counterexample path output function by a simple example and a complex example.