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

Loading...
Thumbnail Image
Date
2004
Authors
Edelkamp, Stefan
Lluch-Lafuente, Alberto
Editors
Contact
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
DOI (citable link)
ArXiv-ID
International patent number
EU project number
Project
Open Access publication
Restricted until
Title in another language
Research Projects
Organizational Units
Journal Issue
Publication type
Journal article
Publication status
Published in
International journal on software tools for technology transfer ; 5 (2004), 2-3. - pp. 247-267
Abstract
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.
Summary in another language
Subject (DDC)
004 Computer Science
Keywords
Model checking,Directed search,Protocol validation
Conference
Review
undefined / . - undefined, undefined. - (undefined; undefined)
Cite This
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. 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>
Internal note
xmlui.Submission.submit.DescribeStep.inputForms.label.kops_note_fromSubmitter
Contact
URL of original publication
Test date of URL
Examination date of dissertation
Method of financing
Comment on publication
Alliance license
Corresponding Authors der Uni Konstanz vorhanden
International Co-Authors
Bibliography of Konstanz
Yes
Refereed