Take a look at the new version of this page: [ beta version ]. Tell us what you think.

ABSTRACT

Protocol validation and verification techniques have been applied successfully for a number of years to a wide range of protocols. The increasing complexity of our communications systems requires us to examine existing techniques and make a realistic assessment of which techniques will be applicable to the complex systems of the future. We believe that validation techniques based on an exhaustive reachability analysis will not be effective. Sampling techniques, such as executing a random walk through the reachable state space, are effective in complex systems, since most protocol errors occur in many different states of the system. More than 10 years have elapsed since the first automated validation techniques were first applied to communications protocols [1,2]. In the meantime, considerable advances have been made in validation technology, but more significantly, the scale and nature of the validation problem have changed. The communications systems that we need to validate today are significantly more complex than those of ten years ago. Our methods must evolve in order to address the current challenge. This paper is concerned primarily with the nature of the validation process, and the results that we might reasonably expect to achieve when validating protocols in complex communications systems.

REFERENCES

• 1: C.H. West and P. Zafiropulo, "Automated validation of a communications protocol'the CCITT X.21 Recommendation," IBM J. Res. Develop., vol. 22, No. 1, January 1978, pp 60-71.
• 2: J. Hajek, "Automatically Verified Data Transfer Protocols," Proceedings of the International Conference on Computer Communications, Kyoto, Japan, pp. 749-756, 1978.
• 3: ISO Open Systems Interconnection, "LOTOS - A Formal Description Technique Based on the Temporal Ordering of Observational Behavior'", Draft Proposed Standard 8807, September 1987.
• 4: ISO Open Systems Interconnection, "Estelle- A Formal Description Technique Based on an Extended State Transition Model'" Draft Proposed Standard 9074 rev, August i 986.
• 5: Simon C. Nash, Format and protocol language (FAPL), Computer Networks and ISDN Systems, v.14 n.1, p.61-77, March, 1987 [doi>10.1016/0169-7552(87)90086-9]
• 6: C.A. Sunshine, "Experience with Automated Protocol Verification," Protocol Specification, Testing and Verification III, North-Holland, Amsterdam, 1985, pp. 229-236.
• 7: Jean-Luc Richier , Carlos Rodriguez , Joseph Sifakis , Jacques Voiron, Verification in XESAR of the Sliding Window Protocol, Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII, p.235-248, May 05-08, 1987
• 8: Ana R. Cavalli , François Horn, Proof of Specification Properties by Using Finite State Machines and Temporal Logic, Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII, p.221-233, May 05-08, 1987
• 9: M.Y. Vardi, "Verification of Concurrent Programs - The Automata Theoretic Framework," Proc. 2nd IEEE Symp. on Logic in Computer Science, Ithaca NY, June 1987, pp. 167-176.
• 10: James,H. Fetzer, Program verification: the very idea, Communications of the ACM, v.31 n.9, p.1048-1063, Sept. 1988 [doi>10.1145/48529.48530]
• 11: M. Sajkowski, "Protocol Verification Techniques' Status Quo and Perspectives," Protocol Specification, Testing and Verification IV, edited by Y. Yemeni, R. Strom and S. Yemeni, North-Holland, Amsterdam, 1985, pp. 697-720.
• 12: Michel Diaz, Modelling and Analysis of Communication and Cooperation Protocols Using Petri Net Based Models, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.465-510, May 17-20, 1982
• 13: G.D. Schultz, D.B. Rose, C.H. West and J.P. Gray, "Executable Representation and Validation of SNA," Computer Network Architectures and Protocols, editor P.E. Green Jr., Plenum Publishing Corporation, New York, 1982, pp. 671-705.
• 14: P. Zafiropulo, "Protocol Validation by Duologue Matrix Analysis," IEEE Trans. Commun., vol. COM-26, No. 8, pp. 1187-1194, August 1978.
• 15: C.H. West, "An Automated Technique for Communications Protocol Validation," IEEE Trans. Commun., vol. COM-26, No. 8, pp. 1271-1275, August 1978.
• 16: C.H. West, "General Technique for Communications Protocol Validation," IBM J. Res. Develop. vol. 22, No. 3, July 1978, pp. 393-404.
• 17: O. Rafiq and J.P. Ansart, "VALIDOC, a Protocol Validator and Its Applications" Protocol Specification, Testing and Verification III, North-Holland, Amsterdam, 1983, pp. 189-197.
• 18: Deepinder P. Sidhu> , Thomas P. Blumer, Automated verification of connection management of NBS class 4 transport protocol, Proceedings of the ACM SIGCOMM symposium on Communications architectures and protocols: tutorials & symposium, p.83-89, June 06-08, 1984, Montréal, Quebec, Canada, United States [doi>10.1145/800056.802064]
• 19: E. Timothy Morgan , Rami R. Razouk, Computer-aided analysis of concurrent systems, Proceedings of the IFIP WG6.1 Fifth International Conference on Protocol Specification, Testing and Verification V, p.49-58, June 10-13, 1985
• 20: F. J. Lin , P. M. Chu , M. T. Liu, Protocol verification using reachability analysis: the state space explosion problem and relief strategies, ACM SIGCOMM Computer Communication Review, v.17 n.5, p.126-135, Oct./Nov. 1987 [doi>10.1145/55483.55496]
• 21: C.H. West and J. Rubin, "An improved Protocol Validation Technique," Computer Networks, Vol. 6, No. 2, pp. 65-74, May 1982.
• 22: M.G. Gouda and Y.T. Yu, "Protocol Validation by Maximal Progress State Exploration," IEEE Trans. Commun., January 1984.
• 23: Gerard J. Holzmann, On Limits and Possibilities of Automated Protocol Analysis, Proceedings of the IFIP WG6.1 Seventh International Conference on Protocol Specification, Testing and Verification VII, p.339-344, May 05-08, 1987
• 24: "Information Processing Systems- Open Services I nterconnection-Basic Connection Oriented Session Protocol Specification," ISO/TC97/SC21 N268 (ISO tS 8326), September 1984.
• 25: 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]
• 26: C H West, A validation of the OSI session layer protocol, Computer Networks and ISDN Systems, v.11 n.3, p.173-182, March 1986 [doi>10.1016/0169-7552(86)90033-4]
• 27: C.H. West "Protocol Validation by Random State Exploration," Protocol Specification, Testing and Verification, Vl, North-Holland, Amsterdam, 1986, pp. 233-242.
• 28: J. Rubin, "Testing Protocols Using Random Legal Inputs," Computer Network Usage: Recent Experiences, Proceedings of the IFIP TC 6 Working Conference COMNET'85 Budapest, Hungary October 1985, published by North-Holland, Amsterdam, 1986.
• 29: W. Feller, "An introduction to Probability Theory and Its Applications," Vol 1. pp. 98-108, John Wiley & Sons, New York, 1968.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.0 General
          Subjects: Open Systems Interconnection reference model (OSI)

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

General Terms:
Algorithms, Verification