Protocol verification using reachability analysis: The state space explosion problem and relief strategies

Fuchun Lin, P. M. Chu, M. T. Liu

研究成果: Conference contribution

74 引文 斯高帕斯(Scopus)

摘要

Reachability analysis has proved to be one of the most effective methods in verifying correctness of communication protocols based on the state transition model. Consequently, many protocol verification tools have been built based on the method of reachability analysis. Nevertheless, it is also well known that state space explosion is the most severe limitation to the applicability of this method. Although researchers in the field have proposed various strategies to relieve this intricate problem when building the tools, a survey and evaluation of these strategies has not been done in the literature. In searching for an appropriate approach to tackling such a problem for a grammar-based validation tool, we have collected and evaluated these relief strategies, and have decided to develop our own from yet another but more systematic approach. The results of our research are now reported in this paper. Essentially, the paper is to serve two purposes: first, to give a survey and evaluation of existing relief strategies; second, to propose a new strategy, called PRO VAT (PROtocol VAlidation Testing), which is inspired by the heuristic search techniques in Artificial Intelligence. Preliminary results of incorporating the PROVAT strategy into our validation tool are reviewed in the paper. These results show the empirical evidence of the effectiveness of the PROVAT strategy.

原文English
主出版物標題Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987
編輯J. J. Garcia-Luna-Aceves
發行者Association for Computing Machinery, Inc
頁面126-135
頁數10
ISBN(電子)0897912454, 9780897912457
DOIs
出版狀態Published - 1 八月 1987
事件1987 ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987 - Stowe, United States
持續時間: 11 八月 198713 八月 1987

出版系列

名字Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987

Conference

Conference1987 ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987
國家United States
城市Stowe
期間11/08/8713/08/87

指紋 深入研究「Protocol verification using reachability analysis: The state space explosion problem and relief strategies」主題。共同形成了獨特的指紋。

  • 引用此

    Lin, F., Chu, P. M., & Liu, M. T. (1987). Protocol verification using reachability analysis: The state space explosion problem and relief strategies. 於 J. J. Garcia-Luna-Aceves (編輯), Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987 (頁 126-135). (Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987). Association for Computing Machinery, Inc. https://doi.org/10.1145/55482.55496