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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

74 Scopus citations

Abstract

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.

Original languageEnglish
Title of host publicationProceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987
EditorsJ. J. Garcia-Luna-Aceves
PublisherAssociation for Computing Machinery, Inc
Pages126-135
Number of pages10
ISBN (Electronic)0897912454, 9780897912457
DOIs
StatePublished - 1 Aug 1987
Event1987 ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987 - Stowe, United States
Duration: 11 Aug 198713 Aug 1987

Publication series

NameProceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987

Conference

Conference1987 ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987
CountryUnited States
CityStowe
Period11/08/8713/08/87

Fingerprint Dive into the research topics of 'Protocol verification using reachability analysis: The state space explosion problem and relief strategies'. Together they form a unique fingerprint.

  • Cite this

    Lin, F., Chu, P. M., & Liu, M. T. (1987). Protocol verification using reachability analysis: The state space explosion problem and relief strategies. In J. J. Garcia-Luna-Aceves (Ed.), Proceedings of the ACM Workshop on Frontiers in Computer Communications Technology, SIGCOMM 1987 (pp. 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