KOPS - Das Institutionelle Repositorium der Universität Konstanz

Directed explicit-statemodel checking in the validation of communication protocols

Directed explicit-statemodel checking in the validation of communication protocols

Zitieren

Dateien zu dieser Ressource

Prüfsumme: MD5:2411d010793ade9ac0507849dc67ac12

EDELKAMP, Stefan, Stefan LEUE, Alberto LLUCH-LAFUENTE, 2004. Directed explicit-statemodel 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

@article{Edelkamp2004Direc-5474, title={Directed explicit-statemodel checking in the validation of communication protocols}, year={2004}, doi={10.1007/s10009-002-0104-3}, 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} }

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. Lluch-Lafuente, Alberto Edelkamp, Stefan 2011-03-24T15:55:42Z First publ. in: International journal on software tools for technology transfer 5 (2004), 2-3, pp. 247-267 2004 eng Leue, Stefan Directed explicit-statemodel checking in the validation of communication protocols deposit-license 2011-03-24T15:55:42Z Edelkamp, Stefan Leue, Stefan Lluch-Lafuente, Alberto application/pdf

Dateiabrufe seit 01.10.2014 (Informationen über die Zugriffsstatistik)

Directed_explicit_statemodel_checking_in_the_validation_of_communication_protocols.pdf 190

Das Dokument erscheint in:

deposit-license Solange nicht anders angezeigt, wird die Lizenz wie folgt beschrieben: deposit-license

KOPS Suche


Stöbern

Mein Benutzerkonto