Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-23404-5_11 | International SPIN Workshop on Model Checking of Software |
Field | DocType | Volume |
Model checking,State space exploration,Automaton,Metric (mathematics),Algorithm,Theoretical computer science,Promela,Rotation formalisms in three dimensions,Mathematics | Conference | 9232 |
ISSN | Citations | PageRank |
0302-9743 | 2 | 0.39 |
References | Authors | |
3 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ahmad Siyar Andisha | 1 | 8 | 1.36 |
| Martin Wehrle | 2 | 118 | 10.37 |
| Bernd Westphal | 3 | 43 | 8.45 |