Research On Parallel Query And Checking Algorithm Of Formal Methods Checking Based On Cloud Computing Platform

With the complication of computer software and hardware systems,formal verification to ensure the safety and reliability of the system becomes a hot-topic.Among them,model checking is receiving attention as a highly automated verification method which used to verify that finite state systems satisfy formal specifications.With the development of formal methods,the constraint increase and the state space is complex.How to speed up the query of large-scale constraint and ensure the efficiency of model checking with complex states has become an urgent need to be solved problem.In the aspect of formal specification,the single-node constrained query method has been unable to efficiently accomplish large-scale query tasks,such as OCL constrained query inefficiency.For formal analysis,the checking of complex system model may lead to the state space explosion problems such as the state space explosion problem for CTL model checking.Relevant research shows that the cloud computing platform can be used to solve the problems faced by the above formal methods and ensure the efficiency of related queries and verification algorithms.Based on this,this thesis proposes an OCL parallel query method based on MapReduce in order to cope with the challenge of mass data and improve the speed of OCL query,this thesis proposes an OCL parallel query method based on MapReduce.By extracting the OCL object attributes set,the queries are converted from the OCL files to the OCL object attributes Set.The experimental results show that using MapReduce to achieve parallel query of object attributes shortens the OCL query time.At the same time,in view of the phenomenon of the state explosion of model checking,a model checking algorithm based on MapReduce rules is designed.This method,combined with the Kripke structure,defines a data structure that is appropriate for MapReduce.This data structure is used to propose a model checking algorithm based on MapReduce.In addition,in view of the poor performance of MapReduce processing iteration data,a parallel CTL model checking algorithm based on HaLoop is proposed.Experiments show that the above methods can greatly alleviate the problem of state explosion.