TY - GEN
T1 - Protocol verification using reachability analysis
T2 - 1987 ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987
AU - Lin, Fuchun
AU - Chu, P. M.
AU - Liu, M. T.
PY - 1987/8/1
Y1 - 1987/8/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85006568223&partnerID=8YFLogxK
U2 - 10.1145/55482.55496
DO - 10.1145/55482.55496
M3 - Conference contribution
AN - SCOPUS:85006568223
T3 - Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987
SP - 126
EP - 135
BT - Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987
A2 - Garcia-Luna-Aceves, J. J.
PB - Association for Computing Machinery, Inc
Y2 - 11 August 1987 through 13 August 1987
ER -