A discipline for constructing multiphase communication protocols

ABSTRACT

Many communication protocols can be observed to go through different phases performing a distinct function in each phase. A multiphase model for such protocols is presented. A phase is formally defined to be a network of communicating finite-state machines with certain desirable correctness properties; these include proper termination and freedom from deadlocks and unspecified receptions. A multifunction protocol is constructed by first constructing separate phases to perform its different functions. It is shown how to connect these phases together to realize the multifunction protocol so that the resulting network of communicating finite state machines is also a phase (i.e., it possesses the desirable properties defined for phases). The modularity inherent in multiphase protocols facilitates not only their construction but also their understanding and modification. An abundance of protocols have been found in the literature that can be constructed as multiphase protocols. Three examples are presented here: two versions of IBM's BSC protocol for data link control and a token ring network protocol.

REFERENCES

• 1: ANDREWS, D.W., AND SCHULTZ, G.D. A token-ring architecture for local area networks: An update. In Proceedings Compcon Fall 82, IEEE, New York, pp. 615-624.
• 2: BRAND, D., AND JOYNER, W.H., JR. Verification of protocols using symbolic execution. Comput. Networks 2, 4/5 (Oct. 1978), 351-360.
• 3: 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]
• 4: BOCHMANN, G.V. Finite state description of communication protocols. Comput, Networks 2, 4/5 (Oct. 1978), 361-372.
• 5: BOCHMANN, G.V., CERNY, E., GAGNE, M., JARD, C., LEVEILLE, A., LACAILLE, C., MAKSUD, M., RAGHUNATHAN, K.S., AND SARIKAYA, B. Experience with formal specifications using an extended state transition model. IEEE Trans. Commun. COM-30, 12 (Dec. 1982), 2506-2513.
• 6: BOCHMANN, G.V., AND SUNSHINE, C. Formal methods in communication protocol design. IEEE Trans. Commun. COM-28, 4 (Apr. 1980), 624-631.
• 7: 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
• 8: Tat Y. Choi , Raymond E. Miller, Network protocol: A structured approach, Proceedings of the 1983 annual conference on Computers : Extending the human resource, p.155-162, January 1983 [doi>10.1145/800173.809721]
• 9: Ching-Hua Chow, A discipline for verification and modular construction of communication protocols (design methodology, tool), 1985
• 10: C. H. Chow , M. G. Gouda , S. S. Lam, An exercise in constructing multi-phase communication protocols, Proceedings of the ACM SIGCOMM symposium on Communications architectures and protocols: tutorials & symposium, p.42-49, June 06-08, 1984, Montréal, Quebec, Canada, United States
• 11: R. J. Cyper, Communications Architecture for Distributed Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1978
• 12: Donald I. Good, Constructing verified and reliable communications processing systems, ACM SIGSOFT Software Engineering Notes, v.2 n.5, p.8-13, October 1977 [doi>10.1145/1005882.1005885]
• 13: GOUDA, M.G. An example for constructing communicating machines by step-wise refinement. In Proceedings 3rd IFIP Workshop on Protocol Specification, Testing, and Verification, H. Rudin and C.H. West, Eds. North-Holland, Amsterdam, 1983, pp. 63-74.
• 14: GOUDA, M.G. Closed covers: To verify progress for communicating finite state machines. IEEE Trans. Softw. Eng. SE-IO, 6 (Nov. 1984), 846-855.
• 15: GOUDA, M.G., AND Vu, Y.T. Protocol validation by maximal progress state exploration. IEEE Trans. Commun. COM-32, 1 (Jan. 1984), 94-97.
• 16: GOUDA, M.G., AND YU, Y.T. Synthesis of communicating machines with guaranteed progress. IEEE Trans. Commun. COM-32, 7 (July 1984), 779-788.
• 17: HAILPERN, B.T., AND OWICKI, S.S. Verifying network protocols using temporal logic. In Proceedings Trends and Applications 1980: Computer Network Protocols, IEEE, New York, 1980, pp. 18-28.
• 18: IBM. General information--Binary synchronous communications. Manual No. GA27-3004-2, 3rd., ed., Oct. 1970.
• 19: Thomas A. Joseph , Thomas Raeuchle , Sam Toueg, State Machines and Assertions (An Integrated Approach to Modeling and Verification of Distributed Systems, Cornell University, Ithaca, NY, 1984
• 20: James F. Kurose, The Specification and Verification of a Connection Establishment Protocol Using Temporal Logic, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.43-62, May 17-20, 1982
• 21: LAM, S.S. Data link control procedures. Computer Communications, Vol. 1: Principles, W. Chou, Ed. Prentice-Hall, Englewood Cliffs, N.J., 1983, pp. 81-113,
• 22: LAM, S.S., AND SHANKAR, A.U. Protocol verification via projections. IEEE Trans. Softw. Eng. SE-IO, 4 (July 1984), 325-342.
• 23: Philip Merlin , Gregor V. Bochmann, On the Construction of Submodule Specifications and Communication Protocols, ACM Transactions on Programming Languages and Systems (TOPLAS), v.5 n.1, p.1-25, Jan. 1983 [doi>10.1145/357195.357196]
• 24: MISRA, J., AND CHANDY, K.M. Proof of networks of processes. IEEE Trans. Softw. Eng. SE-7, 4 (July 1981), 417-426.
• 25: J. Misra , K. M. Chandy , Todd Smith, Proving safety and liveness of communicating processes with examples, Proceedings of the first ACM SIGACT-SIGOPS symposium on Principles of distributed computing, p.201-208, August 18-20, 1982, Ottawa, Canada [doi>10.1145/800220.806698]
• 26: Rami R. Razouk, Modeling X.25 Using the Graph Model of Behavior, Proceedings of the IFIP WG6.1 Second International Workshop on Protocol Specification, Testing and Verification, p.197-214, May 17-20, 1982
• 27: RAZOUK, R.R., AND ESTmN, G. Modeling and verification of communication protocols in SARA: The X.21 interface. IEEE Trans. Comput. C-29, 12 (Dec. 1980), 1038-1052,
• 28: RUBIN, J., AND WEST, C.H. An improved protocol validation technique. Comput. Networks 6, 2 {Apr. 1982), 65-73
• 29: A. Udaya Shankar , Simon S. Lam, An HDLC protocol specification and its verification using image protocols, ACM Transactions on Computer Systems (TOCS), v.1 n.4, p.331-368, Nov. 1983 [doi>10.1145/357377.357384]
• 30: SHANKAR, A.U., AND LAM, S.S. Time-dependent communication protocols. In Principles of Communication and Networking Protocols, S.S. Lam, Ed. IEEE Computer Society Press, New York, 1984, pp. 504-520.
• 31: STENNING, N.Y. A data transfer protocol. Comput. Networks 1, {Sept. 1976), 99-110.
• 32: WEST, C.H., AND ZAPIROPDLO, P. Automated validation of a communications protocol: The CCITT X.21 recommendations. IBM J. Res. Devel. 22 (Jan. 1978), 60-71.
• 33: Yu, Y.T., AND GOUDA, M.G. Deadlock detection for a class of communicating finite state machines. IEEE Trans. Commun. COM-30, (Dec. 1982), 2514-2519.
• 34: Yu, Y.T., AND GOUDA, M.G. Unboundedness detection for a class of communicating finitestate machines. Inf. Proc. Lett. 17 (Dec. 1983), 235-240.
• 35: ZAFIROPULO, P., WEST, C.H., RUDIN, H., COWAN, D.D., AND BRAND, D. Towards analyzing and synthesizing protocols. IEEE Trans. Commun. COM-28, 4 (Apr. 1980), 651-661.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.2 Network Protocols
          Subjects: Protocol architecture (OSI model)

Additional Classification:
  B. Hardware
  B.4 INPUT/OUTPUT AND DATA COMMUNICATIONS
      B.4.4 Performance Analysis and Design Aids**
          Subjects: Verification**; Formal models**

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

  D. Software
  D.1 PROGRAMMING TECHNIQUES
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Structured programming**; Modules and interfaces
      D.2.4 Software/Program Verification
          Subjects: Validation; Correctness proofs

General Terms:
Algorithms, Design, Theory, Verification