Directed Model Checking for PROMELA with Relaxation-Based Distance Functions

Andisha, Ahmad Siyar and Wehrle, Martin and Westphal, Bernd. (2015) Directed Model Checking for PROMELA with Relaxation-Based Distance Functions. In: Model checking software : 22nd international symposium, SPIN 2015). Cham, pp. 153-159.

Full text not available from this repository.

Official URL: http://edoc.unibas.ch/43149/

Downloads: Statistics Overview


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.
Faculties and Departments:05 Faculty of Science > Departement Mathematik und Informatik > Informatik > Artificial Intelligence (Helmert)
UniBasel Contributors:Wehrle, Martin
Item Type:Conference or Workshop Item, refereed
Conference or workshop item Subtype:Conference Paper
Series Name:Lecture Notes in Computer Science
Note:Publication type according to Uni Basel Research Database: Conference paper
Identification Number:
Last Modified:11 Oct 2017 12:09
Deposited On:11 Oct 2017 12:09

Repository Staff Only: item control page