Finding short counterexamples in promela models using estimation of distribution algorithms
Jan Staunton, John A. Clark · 2011
Model checking is an automatic technique that exhaustively checks the state space of a system/program to prove if a specification is satisfied. If an error is detected, the precise circumstances of the issue are returned to the user in the form of a counterexample. Exhaustively checking the state space of a large system, a system with many concurrent components for example, is often intractable. In this scenario, heuristic mechanisms can be employed with the task of detecting errors rather than proving the system is correct. Recently, a metaheuristic EDA-based approach to detecting deadlock in multithreaded Java software has shown great promise in this area. In this paper, we extend that work to search Promela models for counterexamples. We show that the EDA-based technique can find errors where algorithms such as A* search fail. We also show the ability of the EDA to find shorter errors than those discovered by traditional heuristic methods.