Publikation: Protocol Verification with Heuristic Search
Dateien
Datum
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
Internationale Patentnummer
Link zur Lizenz
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Publikationsstatus
Erschienen in
Zusammenfassung
We present an approach to reconcile explicit state model checking and heuristic directed search. We 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.
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
Schlagwörter
Konferenz
Rezension
Zitieren
ISO 690
EDELKAMP, Stefan, Alberto LLUCH-LAFUENTE, Stefan LEUE, 2001. Protocol Verification with Heuristic Search. AAAI. Stanford, California, 26. März 2001 - 28. März 2001. In: Model-based validation of intelligence : papers from the 2001 AAAI symposium ; March 26 - 28, Stanford, California, 2001. 2001BibTex
@inproceedings{Edelkamp2001Proto-5531, year={2001}, title={Protocol Verification with Heuristic Search}, booktitle={Model-based validation of intelligence : papers from the 2001 AAAI symposium ; March 26 - 28, Stanford, California, 2001}, author={Edelkamp, Stefan and Lluch-Lafuente, Alberto and Leue, Stefan} }
RDF
<rdf:RDF xmlns:dcterms="http://purl.org/dc/terms/" xmlns:dc="http://purl.org/dc/elements/1.1/" xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#" xmlns:bibo="http://purl.org/ontology/bibo/" xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#" xmlns:foaf="http://xmlns.com/foaf/0.1/" xmlns:void="http://rdfs.org/ns/void#" xmlns:xsd="http://www.w3.org/2001/XMLSchema#" > <rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/5531"> <dc:contributor>Edelkamp, Stefan</dc:contributor> <dcterms:abstract xml:lang="eng">We present an approach to reconcile explicit state model checking and heuristic directed search. We 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.</dcterms:abstract> <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5531/1/Protocol_Verification_with_Heuristic_Search.pdf"/> <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5531"/> <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by-nc-nd/2.0/"/> <dc:rights>Attribution-NonCommercial-NoDerivs 2.0 Generic</dc:rights> <dc:format>application/pdf</dc:format> <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dc:creator>Leue, Stefan</dc:creator> <dc:creator>Edelkamp, Stefan</dc:creator> <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:15Z</dc:date> <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/> <dc:language>eng</dc:language> <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5531/1/Protocol_Verification_with_Heuristic_Search.pdf"/> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:contributor>Leue, Stefan</dc:contributor> <dc:contributor>Lluch-Lafuente, Alberto</dc:contributor> <dcterms:bibliographicCitation>First publ. in: Model-based validation of intelligence : papers from the 2001 AAAI symposium ; March 26 - 28, Stanford, California, 2001</dcterms:bibliographicCitation> <dc:creator>Lluch-Lafuente, Alberto</dc:creator> <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:56:15Z</dcterms:available> <foaf:homepage rdf:resource="http://localhost:8080/"/> <dcterms:title>Protocol Verification with Heuristic Search</dcterms:title> <dcterms:issued>2001</dcterms:issued> </rdf:Description> </rdf:RDF>