Parallelizing random-walk based model checking

Abstract

In model checking, a formal methods technique to verify a system with some desired properties, the guidance techniques have been employed a long time ago in driving the verification into area of `error` in the state space. Another technique is to choose the next state to be explored in a walk randomly to avoid the `wrong` guidance. When the latter is a nonexhaustive technique in the sense that only a manageable number of walks are carried out before the search is terminated, it does scale well. In enhancing the technique to use recently powerful parallel/multi-core systems, research on parallelizing the algorithm shall be carried out. In this work, we propose a method that parallelizes the random-walk algorithm. It also increases the completeness of the non-exhaustive algorithm. The experimentation has shown the great improvement of the proposed algorithm compares to the original once.