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

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 PROVAT (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.

REFERENCES

• 1: Jean-Pierre Ansart, Issues and Tools for Protocol Specification, Distributed Systems: Methods and Tools for Specification, An Advanced Course, April 3-12, 1984 and April 16-25, 1985 Munich, p.481-538, January 1985
• 2: A. Gardner. Search. The Handbook of Artificial Intelligence. William Kaufman, 1981, Chapter 1I.
• 3: Thomas P. Blumer , Deepinder P. Sidhu, Mechanical verification and automatic implementation of communication protocols, IEEE Transactions on Software Engineering, v.12 n.8, p.827-843, Aug. 1986
• 4: Daniel Brand , Pitro Zafiropulo, On Communicating Finite-State Machines, Journal of the ACM (JACM), v.30 n.2, p.323-342, April 1983 [doi>10.1145/322374.322380]
• 5: Tat Y. Choi , Raymond E. Miller, A decomposition method for the analysis and design of finite state protocols, Proceedings of the eighth symposium on Data communications, p.167-176, October 03-06, 1983, North Falmouth, Massachusetts, United States
• 6: Ching-Hua Chow , Mohamed G. Gouda , Simon S. Lam, A discipline for constructing multiphase communication protocols, ACM Transactions on Computer Systems (TOCS), v.3 n.4, p.315-343, Nov. 1985 [doi>10.1145/6110.214400]
• 7: M.G. Gouda and Y. T. Yu. Protocol Validation by Maximal Progress State Exploration. IEEE Trans. on Communications COM-32(1):94-97, Janunary, 1984.
• 8: M.G. Gouda and J.-Y. Han. Protocol Validation by Fair Progress State Exploration. Computer Networks and ISDN Systems 9:353-361, 1985.
• 9: G.J. Holzmann. Tracing Protocol. AT~T Technical Journal 64(10):2413-2433, December, 1985.
• 10: Gerard J. Holzmann, Automated protocol validation in Argos: assertion proving and scatter searching, IEEE Transactions on Software Engineering, v.13 n.6, p.683-696, June 1987 [doi>10.1109/TSE.1987.233206]
• 11: Ellis Horowitz , Sartaj Sahni, Fundamentals of Computer Alori, W. H. Freeman & Co., New York, NY, 1978
• 12: M. I~oh and H. Ichikawa. Protocol Verification Algorithm Using Reduced Reachability Analysis. The Trans. on the IECE of Japan E66(2):88-93, February, 1983.
• 13: Y. Kakuda, Y. Wakahara, and M. Norigoe. A New Algorithm for Fast Protocol Validation. In Proc. COMPSAC, pages 228-236. {EEE, 1986.
• 14: S.S. Lam and A. U. Shanker. Protocol Verification via Projections. IEEEE Trans. on Software Engineering SE-10(4):325-342, July, 1984.
• 15: F.J. Lin, P. M. Chu, and M. T. Liu. Probabilistic Transmission Grammmar. I987 Unpublished Notes.
• 16: c.s. L~. Automated Validation o{ Communication Protocols. PhD thesis, The Ohio State Univ., 1986.
• 17: Judea Pearl, Heuristics: intelligent search strategies for computer problem solving, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1984
• 18: S. Purushothaman , P. A. Subrahmanyam, Reasoning about probabilistic behavior in concurrent systems, IEEE Transactions on Software Engineering, v.13 n.6, p.740-745, June 1987 [doi>10.1109/TSE.1987.233478]
• 19: J. Rubin and C. H. West. An Improved Protocol Validation Technique. Computer Networks 6:65-73, 1982.
• 20: A.Y. Teng and M. T. Liu. The Transmission Grammar Model for Protocol Construction. {n Proc. Trends and Applications Symposium, pages 110-120. NBS~ 1980.
• 21: Lloyd David Umbaugh, Automated techniques for specification and validation of communications protocols, 1983
• 22: S.T. Vuong and D. D. Cowan. A Decomposition Method for the Validation of Structured Protocols. In Proc. {NFOCOM, pages 209-220. IEEE, 1982.
• 23: S.T. Vuong, D. D. tiui, and D. D. Cowan. VALIRA- A Tool for Protocol Validation Via Reachability Analysis. Protocol Specification, Testing, and Verificatior~, North-Holland, 1987, pages 35-41.
• 24: C.H. West and P. Zafiropulo. Automated Validation of a Communication Protocol: the CCITT X.21 Recommendation. IBM dourr~al of Research and Development 22(1):60-71, 1978.
• 25: Colin H. West, Applications and Limitations of Automated Protocol Validation, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.361-371, May 17-20, 1982
• 26: C.H. West. Protocol Validation by Random State Exploration. Protocol Specification, Testing, and Verification, VI. North-Holland, t987, pages 233-242.
• 27: P. Zafiropulo, C. H. West, ~. Rudin, D. D. Cowan, and D. Brand. Towards Analyzing and Synthesizing Protocols. IEEE Trans. on Communication 28(4):651-660, April, 1980.
• 28: J.-R. Zhao and G. V. Bochmann. Reduced Reachability Analysis of Communicaiton Protocols : A New Approach. Protocol Specification, Testing, and Verification, VI. North-Holland, 1987. pages 243-254.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol verification

Additional Classification:
  K. Computing Milieux
  K.1 THE COMPUTER INDUSTRY
      Subjects: Standards

General Terms:
Standardization, Verification