Journal article
Trail-Directed Model Checking
Institut für Informatik Albert-Ludwigs-Universität Georges-Köhler-Allee D-79110 Freiburg, Germany
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.
Language: | English |
---|---|
Year: | 2001 |
Pages: | 343-356 |
ISSN: | 15710661 |
Types: | Journal article |
DOI: | 10.1016/S1571-0661(04)00261-0 |