Abstract: This paper reports on the basic concepts, methods and techniques of reachability analysis verification for communication protocols. Through a practical reachability analysis automation system developed by the authors, the construction of automation system, the algorithms for state space extension and some techniques to avoid "state space explosion" are also presented.