Directed explicit-state model checking in the validation of communication protocols

Lade...
Vorschaubild
Datum
2004
Autor:innen
Edelkamp, Stefan
Lluch-Lafuente, Alberto
Herausgeber:innen
Kontakt
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
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
Forschungsvorhaben
Organisationseinheiten
Zeitschriftenheft
Publikationstyp
Zeitschriftenartikel
Publikationsstatus
Published
Erschienen in
Zusammenfassung

The success of model checking is largely based on its ability to efficiently locate errors in software designs. If an error is found, a model checker produces a trail that shows how the error state can be reached, which greatly facilitates debugging. However, while current model checkers find error states efficiently, the counterexamples are often unnecessarily lengthy, which hampers error explanation. This is due to the use of naive search algorithms in the state space exploration. In this paper we present approaches to the use of heuristic search algorithms in explicit-state model checking. We present the class of A∗ directed search algorithms and propose heuristics together with bitstate compression techniques for the search of safety property violations.
We achieve great reductions in the length of the error trails, and in some instances render problems analyzable by exploring a much smaller number of states than standard depth-first search.We then suggest an improvement of the nested depth-first search algorithm and show how it can be used together with A∗ to improve the search for liveness property violations. Our approach to directed explicit-state model checking has been implemented in a tool set called HSF-SPIN.We provide experimental results from the protocol validation domain using HSF-SPIN.

Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
Model checking, Directed search, Protocol validation
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690EDELKAMP, Stefan, Stefan LEUE, Alberto LLUCH-LAFUENTE, 2004. Directed explicit-state model checking in the validation of communication protocols. In: International journal on software tools for technology transfer. 2004, 5(2-3), pp. 247-267. Available under: doi: 10.1007/s10009-002-0104-3
BibTex
@article{Edelkamp2004Direc-5474,
  year={2004},
  doi={10.1007/s10009-002-0104-3},
  title={Directed explicit-state model checking in the validation of communication protocols},
  number={2-3},
  volume={5},
  journal={International journal on software tools for technology transfer},
  pages={247--267},
  author={Edelkamp, Stefan and Leue, Stefan and Lluch-Lafuente, Alberto}
}
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/5474">
    <bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/5474"/>
    <dc:format>application/pdf</dc:format>
    <dspace:hasBitstream rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5474/1/Directed_explicit_statemodel_checking_in_the_validation_of_communication_protocols.pdf"/>
    <dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:42Z</dcterms:available>
    <dc:creator>Edelkamp, Stefan</dc:creator>
    <dcterms:abstract xml:lang="eng">The success of model checking is largely based on its ability to efficiently locate errors in software designs. If an error is found, a model checker produces a trail that shows how the error state can be reached, which greatly facilitates debugging. However, while current model checkers find error states efficiently, the counterexamples are often unnecessarily lengthy, which hampers error explanation. This is due to the use of  naive  search algorithms in the state space exploration. In this paper we present approaches to the use of heuristic search algorithms in explicit-state model checking. We present the class of A∗ directed search algorithms and propose heuristics together with bitstate compression techniques for the search of safety property violations.&lt;br /&gt;We achieve great reductions in the length of the error trails, and in some instances render problems analyzable by exploring a much smaller number of states than standard depth-first search.We then suggest an improvement of the nested depth-first search algorithm and show how it can be used together with A∗ to improve the search for liveness property violations. Our approach to directed explicit-state model checking has been implemented in a tool set called HSF-SPIN.We provide experimental results from the protocol validation domain using HSF-SPIN.</dcterms:abstract>
    <dcterms:bibliographicCitation>First publ. in: International journal on software tools for technology transfer 5 (2004), 2-3, pp. 247-267</dcterms:bibliographicCitation>
    <dcterms:hasPart rdf:resource="https://kops.uni-konstanz.de/bitstream/123456789/5474/1/Directed_explicit_statemodel_checking_in_the_validation_of_communication_protocols.pdf"/>
    <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
    <dc:language>eng</dc:language>
    <foaf:homepage rdf:resource="http://localhost:8080/"/>
    <dc:contributor>Lluch-Lafuente, Alberto</dc:contributor>
    <dc:rights>Attribution-NonCommercial-NoDerivs 2.0 Generic</dc:rights>
    <dc:contributor>Edelkamp, Stefan</dc:contributor>
    <dcterms:rights rdf:resource="http://creativecommons.org/licenses/by-nc-nd/2.0/"/>
    <dc:creator>Lluch-Lafuente, Alberto</dc:creator>
    <dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-24T15:55:42Z</dc:date>
    <dc:contributor>Leue, Stefan</dc:contributor>
    <dcterms:issued>2004</dcterms:issued>
    <dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
    <dcterms:title>Directed explicit-state model checking in the validation of communication protocols</dcterms:title>
    <dc:creator>Leue, Stefan</dc:creator>
  </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
Ja
Begutachtet
Diese Publikation teilen