An Approach to Improving Reliability of Parallel Graph Computation

The distributed programming framework for parallel graph computation has been proposed to process and analyze large scale graph data. However, how to model and verify properties of parallel graph computation deserves our attention and studying so as to improve the reliability of big data processing. In this paper, we propose an approach based on runtime verification at code level to verify properties of the parallel graph computation process. With this approach, the parallel computation framework Pregel for graph data processing is modeled in MSVL (Modeling, Simulation and Verification Language), a property to be verified is specified by a PPTL (Propositional Projection Temporal Logic) formula, then a compiler MCII is employed to verify whether a property is satisfied. Case studies of the shortest path problem and PageRank algorithm are conducted to demonstrate our approach.