Directed explicit-state model checking in the validation of communication protocols
Directed explicit-state model checking in the validation of communication protocols
Loading...
Date
2004
Authors
Editors
Journal ISSN
Electronic ISSN
ISBN
Bibliographical data
Publisher
Series
URI (citable link)
DOI (citable link)
International patent number
Link to the license
EU project number
Project
Open Access publication
Collections
Title in another language
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.
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 690
EDELKAMP, 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-3BibTex
@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.<br />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
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