Directed Model Checking for PROMELA with Relaxation-Based Distance Functions

Directed model checking uses distance functions to guide the state space exploration to efficiently find short error paths. Distance functions based on delete-relaxation have successfully been used for, e. g., model checking timed automata. However, such distance functions have not been investigated for formalisms with rich expression languages as provided by PROMELA. We present a generalization of delete-relaxation-based distance functions to a subclass of PROMELA. We have evaluated the resulting search behavior on a large number of models from the BEEM database within the HSF-SPIN model checker. Our experiments show significantly better guidance compared to the previously best distance function available in HSF-SPIN.