Protocol Verification with Heuristic Search

Stefan Edelkamp, Alberto Lluch Lafuente, Stefan Leue

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

We present an approach to reconcile explicit state model checking and heuristic directed search and provide experimental evidence that the model checking problem for concurrent systems, such as communications protocols, can be solved more efficiently, since finding a state violating a property can be understood as a directed search problem. In our work we combine the expressive power and implementation efficiency of the SPIN model checker with the HSF heuristic search workbench, yielding the HSF-SPIN tool that we have implemented. We start off from the A* algorithm and some of its derivatives and define heuristics for various system properties that guide the search so that it finds error states faster. In this paper we focus on safety properties and provide heuristics for invariant and assertion violation and deadlock detection. We provide experimental results for applying HSF-SPIN to two toy protocols and one real world protocol, the CORBA GIOP protocol.
Original languageEnglish
Title of host publicationProceedings of the AAAI Spring Symposium on Model-Based Validation of Inteligence
Publication date2001
ISBN (Print)1-57735-132-0
Publication statusPublished - 2001
Externally publishedYes
EventAAAI Spring Symposium on Model-Based Validation of Intelligence - Stanford, United States
Duration: 26 Mar 200128 Mar 2001

Conference

ConferenceAAAI Spring Symposium on Model-Based Validation of Intelligence
CountryUnited States
CityStanford
Period26/03/200128/03/2001

Cite this

Edelkamp, S., Lluch Lafuente, A., & Leue, S. (2001). Protocol Verification with Heuristic Search. In Proceedings of the AAAI Spring Symposium on Model-Based Validation of Inteligence