Abstract
HSF-SPIN is a Promela model checker based on heuristic search strategies. It utilizes heuristic estimates in order to direct the search for finding software bugs in concurrent systems. As a consequence, HSF-SPIN is able to find shorter trails than blind depth-first search.
This paper contributes an extension to the paradigm of directed model checking to shorten already established unacceptable long error trails. This approach has been implemented in HSF-SPIN. For selected benchmark and industrial communication protocols experimental evidence is given that trail-directed model-checking effectively shortcuts existing witness paths.
This paper contributes an extension to the paradigm of directed model checking to shorten already established unacceptable long error trails. This approach has been implemented in HSF-SPIN. For selected benchmark and industrial communication protocols experimental evidence is given that trail-directed model-checking effectively shortcuts existing witness paths.
| Original language | English |
|---|---|
| Journal | Theoretical Computer Science |
| Volume | 55 |
| Issue number | 3 |
| Pages (from-to) | 343-356 |
| ISSN | 0304-3975 |
| DOIs | |
| Publication status | Published - 2001 |
| Externally published | Yes |
| Event | 1st Workshop on Software Model Checking - , Denmark Duration: 1 Oct 2001 → 1 Oct 2001 Conference number: 1 |
Conference
| Conference | 1st Workshop on Software Model Checking |
|---|---|
| Number | 1 |
| Country/Territory | Denmark |
| Period | 01/10/2001 → 01/10/2001 |