Directed search for the verification of communication protocols

There is a need for formal methods to verify correctness of software <br>and hardware systems. Automated verification techniques basically <br>explore the state space of a system in order to establish whether or <br>not it behaves correctly. The main drawback of such methods is the state explosion problem. The size of the state space can grow <br>exponentially in the number of components of the system, especially in <br>asynchronous concurrent systems. In early stages of system <br>development, errors are likely to appear. As a matter of fact, in practice, <br>automated verification has been shown to be more successful in finding errors in <br>systems than in proving correctness. Usually, one applies reachability algorithms like <br>depth-first, and breadth-first search for this purpose. Breadth-first <br>search is, in general, not memory-efficient, but offers shortest <br>counterexamples. On the other hand, depth-first search is more <br>memory-efficient, but delivers suboptimal counterexamples. <br> <br>We propose and analyze the use of classic heuristic search <br>algorithms for a more efficient error detection. First, heuristic <br>search can help mitigate the effects of the state explosion <br>problem by guidining the search into error states. Second, some of these <br>algorithms can guarantee optimal counterexamples. This is important <br>for the error correction process since, in general, the shorter a <br>counterexample is, the easier it is to understand what it really means. <br> <br>We distinguish two main problems: finding an error quickly, and <br>finding a short(est) counterexample. Each problem has different <br>requirements and calls for different strategies. <br>Heuristic functions are applied to guide the search. We propose <br>and analyze several such functions. Moreover, we analyze how heuristic <br>search combines with other techniques usually applied to avoid the <br>state explosion problem, namely partial order reduction and bitstate hashing. <br> <br>We basically concentrate on the detection of <br>safety errors, which are just reach

Author dc:creator

• Lluch Lafuente, Alberto

Contributors dc:contributor

• Ottmann, Thomas

Repository record source_url

https://freidok.uni-freiburg.de/data/791

OAI identifier oai:identifier

oai:freidok.uni-freiburg.de:791