Formal Verification Based on Guided Random Walks

Abstract

In software development, formal verification and simulation are seen as complimentary paradigms: the former can guarantee the correctness of systems with respect to properties, but does not scale; the latter does scale but cannot guarantee the absent of errors. In the authors’ previous work, a mechanism of statically analysing a model has been used to build an abstraction of the original model, which in turn is used to guide a heuristic search in a guided model checker. We extend that work and apply the same technique to build a heuristically-driven, or guided, random-walk model checker. This work sits at the intersection of a number of research areas: model checking, random walks, heuristic search and simulation. Novel here is the use of a heuristic mechanism to guide the random walk towards states of the model that possibly violate user-defined properties, and the use of an automatic abstraction scheme to build the heuristic. In a series of experiments, we compare the performance of our guided, random-walk based tool to standard model-checking tools. A new metric that we call Process Error Participation (PEP) has also been devised to classify model behaviour.