Improving software model checking on program backbone within distributed system

Model checking technique currently has been applied to a wide range of problem domains. Among them, verifying the reliability of software systems becomes much more significant. However, as to software with complex structure and large scale, the verification process suffers from the state space explosion, thus leading to the resource exhaustion and low efficiency. In this paper, we propose a method of improving software model checking in both foreground and background of ANSI-C source program to verify the properties. In the foreground stage, we directly dispose of program itself by pruning the program with respect to the assertion property and compressing the circular paths to extract the program backbone. Subsequently, the program backbone is used to generate a simple CTL automaton model which will be applied afterwards. In the background stage, we redesign the CTL state automaton's data structure and improve the model checking algorithm to adapt the MapReduce framework in distributed system. The set of states which are satisfied with CTL property is output and checked for satisfiability based on the CTL automaton model. The example in each part illustrates the validity of the whole method, and the experiments show this method improves the efficiency of program verification substantially.