Publikation:

Protocol Verification with Heuristic Search

Lade...
Vorschaubild

Dateien

Protocol_Verification_with_Heuristic_Search.pdf
Protocol_Verification_with_Heuristic_Search.pdfGröße: 286.46 KBDownloads: 368

Datum

2001

Autor:innen

Edelkamp, Stefan
Lluch-Lafuente, Alberto

Herausgeber:innen

Kontakt

ISSN der Zeitschrift

Electronic ISSN

ISBN

Bibliografische Daten

Verlag

Schriftenreihe

Auflagebezeichnung

DOI (zitierfähiger Link)
ArXiv-ID

Internationale Patentnummer

Angaben zur Forschungsförderung

Projekt

Open Access-Veröffentlichung
Open Access Green
Core Facility der Universität Konstanz

Gesperrt bis

Titel in einer weiteren Sprache

Publikationstyp
Beitrag zu einem Konferenzband
Publikationsstatus
Published

Erschienen in

Model-based validation of intelligence : papers from the 2001 AAAI symposium ; March 26 - 28, Stanford, California, 2001. 2001

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)
004 Informatik

Schlagwörter

Konferenz

AAAI, 26. März 2001 - 28. März 2001, Stanford, California
Rezension
undefined / . - undefined, undefined

Forschungsvorhaben

Organisationseinheiten

Zeitschriftenheft

Zugehörige Datensätze in KOPS

Zitieren

ISO 690EDELKAMP, 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. 2001
BibTex
@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>

Interner Vermerk

xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter

Kontakt
URL der Originalveröffentl.

Prüfdatum der URL

Prüfungsdatum der Dissertation

Finanzierungsart

Kommentar zur Publikation

Allianzlizenz
Corresponding Authors der Uni Konstanz vorhanden
Internationale Co-Autor:innen
Universitätsbibliographie
Nein
Begutachtet
Diese Publikation teilen