Research On Software Model Checking Acceleration Method Of Distributed System

Software model checking attracts more and more attention and it has more significance to check the reliability of software systems, whereas the verification process would cause the problem named state space explosion especially in the large scale software with complex data structure. Distributed system can accelerate verification speed to a certain extent, but its instability could also cause much lower efficiency and exhaust the resource. Therefore, my research focuses on the how to draw the significant parts, how to transplant the model checking problem to distributed system area. It has special research significance and application value on improving verification efficiency and expanding code scale.Firstly, an improved software model checking method has been presented in both front-end with back-end. In the front-end stage, the method directly handles with software program by cutting it into pieces and reducing circulation space to simplify the standard C source program, so as to obtain the program core. And then, the state division has been done in order to generate a much simpler automaton CTL model. Afterwards, getting into back-end stage, it can be moved forward by redesigning the CTL state automaton’s data structure and improving labeling algorithm, so as to make the model checking problem adapte MapReduce structure in Hadoop cluster. After distributed accelerating calculation, it can output the set of states satisfied with the property. Meanwhile, aiming at the failure of distributed system problem, the Zookeeper watching system in distributed system has been written to check nodes. The watching system can automatically replace spare node to ensure the calculation speed.Using the programming interface of distributed system Hadoop, Several testing cases have been designed and implemented under the whole method process. Combined with Zookeeper’s watching system, the efficiency of checking method can be further improved. Finally, it proves that proposal improves the verification efficiency strongly by analyzing several examples to illustrate the validity of the whole proposal. Compared with traditional common method, the method can substantially improve the effectiveness and robustness within distributed system.