Heuristic Sensitivity in Guided Random-Walk Based Model Checking

In this work we combine the complementary worlds of model checking and simulation. Model checking is used to verify that a model of a system satisfies some property. In general it considers all inputs. In simulation, a model of a system is executed for particular inputs. Our combined approach, referred to here as formal model simulation, uses the same formal model as model checking, but abandons the notion of verification, which seeks to prove that there are no errors in the model, and instead uses a guided random-walk search algorithm to find errors. The ´guide´ is provided by an abstraction of the system, which for the purposes of this work, is done by hand. Normally it would be automatically generated by analysing the model. We implement the approach in a tool called granSPIN, and in a series of experiments, compare the performance of granSPIN against the conventional model checker SPIN. Novel here is the use of a heuristic to guide the random walk towards states of the model that possibly violate user-defined properties. We also confirm in this work an earlier proposed characterisation called the process error participation factor. This is a more thorough and extensive report of work that was briefly reported earlier.