Research And Implementation Of Temporal Logic Model Checking Algorithm Based On Cloud Computing Platform

To ensure the security by formal verification of dynamic, concurrent and real-time systems has been the focus of software engineering research for several decades.Model checking proposed by Edmund M. Clark, Allen Emerson and Joseph Sifakis in the eighties of the 20 th century is a distinguished formal verification technology,which automatically verifies whether the communication protocol or the system model of a software satisfies a given specification by explicit type of search or implicit fixpoint computation. Model checking becomes very popular and widely used in industry because of its high degree of automation, because of which the proposers won the Turing award in 2007. But the state space of the model checking is increased exponentially with the increasement of system components. This problem is called the state space explosion problem. How to solve the problem of state space explosion of model checking is a research hotspot of scientists and scholars at present.Under the background of the age of big data and Internet+, cloud computing develops rapidly with each passing day. Cloud computing which extends the required hardware and software resources employing virtualization technology greatly improves the computing power and also provides new potential solutions for the state space explosion problem of model checking.The research status of model checking based on temporal logic at home and abroad research status is firstly summarized. After then, the origin and development of the development of cloud computing and big data are studied in depth so as to fully understand the status quo and application background of cloud computing. In general,different cloud computing platforms implement parallel distributed computations based on different models because of which no one can be directly used for model checking and usually it is essential to analysis the problems from scratch. This is the main problem to be researched and solved for this paper. At present, the model checking method based on cloud computing platform mainly employs Hadoop which implements the parallel computational model MapReduce. However, Hadoop isdesigned to solve the problem of batch processing of big data inherently, supporting iterative computation poorly. In fact, temporal logic model checking method can be reduced to graph computation. There usually exist many iterations in the computation process, because of which tmodel checking based on Hadoop usually has a high delay.In order to solve this problem above, a temporal logic model checking method based on BSP model is proposed, a system model of a model checker based on the cloud computing platform Giraph is designed and the pseudo mode of which is implemented in this paper. The control experiments on the same hardware show that the method proposed in this paper is much better than the method based on Hadoop.This is the main innovation of this paper.The work mentioned above has further improved the theoretical system and technical category of the model checking based on the cloud computing platform.