An exercise in constructing multi-phase communication protocols

ABSTRACT

Many real-life protocols can be observed to go through different phases performing a distinct function in each phase. We present a multi-phase model for such protocols. 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 multi-function protocol is constructed by first constructing separate phases to perform its different functions. We discuss how to connect these phases together to implement the multi-function protocol such that the resulting network of communicating finite state machines is also a phase (i.e. it possesses the desirable properties defined for phases). A high-level session control protocol modeled after one in IBM's Systems Network Architecture is discussed, and constructed as a multi-phase protocol.

REFERENCES

• 1: Bochmann, G. V. "Finite State description of communication protocols," Computer Networks, Vol. 2, 1978, pp. 361-371.
• 2: Bochmann, G. V. and C. Sunshine, "Formal methods in communication protocol design," IEEE Trans. on Commun., April 1980, pp.624-631.
• 3: Bochmann, G. V. et al, "Experience with formal specifications using an extended state transition model," IEEE Trans. on Commun., Dec. 1982, pp. 2506-2513.
• 4: Brand, D. and W. H. Joyner, Jr., "Verification of protocols using symbolic execution," Comput. Networks, vol. 2, Oct. 1978, pp.351-360.
• 5: 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]
• 6: C. H. Chow , Mohamed G. Gouda , Simon S. Lam, A Discipline for Constructing Multi-phase Communication Protocols, University of Texas at Austin, Austin, TX, 1983
• 7: R. J. Cyper, Communications Architecture for Distributed Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1978
• 8: 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]
• 9: Gouda, M. G. and Y. T. Yu, "Synthesis of communicating machines with guaranteed progress", TR-179, Dept. of Computer Sciences, Univ. of Texas at Austin, June 1981. Revised Jan. 1983, Oct. 1983. To appear in IEEE Trans. on Commun.
• 10: Mohamed G. Gouda, Closed Covers: to Verify Progress for Communicating Finite State Machines, University of Texas at Austin, Austin, TX, 1982
• 11: Mohamed G. Gouda , E. G. Manning , Y. T. Yu, On the Progress of Communication Between Two Machines, University of Texas at Austin, Austin, TX, 1982
• 12: Mohamed G. Gouda , Y. T. Yu, Protocol Validation by Maximal Progress State Exploration, University of Texas at Austin, Austin, TX, 1982
• 13: Gouda, M. G., "An example for constructing communicating machines by step-wise refinement," Proc. 3rd IFIP Workshop on Protocol Specification, Testing, and Verification, edited by H. Rudin and C. H. West, North-Holland, 1983, pp. 63-74.
• 14: Hailpern, B. T. and S. S. Owicki, "Verifying network protocols using temporal logic," In Proceedings Trends and Applications 1980: Computer Network Protocols, IEEE Computer Society, 1980, pp. 18-28.
• 15: IBM Corp., "General Information-Binary Synchronous Communications," Manual No. GA27-3004-2, 3rd. ed., Oct. 1970.
• 16: Lam, S. S. and A. U. Shankar, "Protocol projections: a method for analyzing communication protocols," Conf. Rec. National Telecommunications Conference, Nov. 1981, New Orleans.
• 17: Simon S. Lam , A. U Shankar, Protocol Verification Via Projections, University of Texas at Austin, Austin, TX, 1982
• 18: Lam, S. S., "Data link control procedures," in Computer Communications, Vol. 1, ed. W. Chou, Prentice-Hall, Englewood Cliffs, 1983, pp. 81-113.
• 19: 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]
• 20: Misra, J. and K. M. Chandy, "Proof of networks of processes," IEEE Tran. on Software Eng., Vol. SE-7, No. 4, July 1981.
• 21: 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]
• 22: Razouk, R. R. and G. Estrin, "Modeling and verification of communication protocols in SARA: The X.21 interface," IEEE Trans. on Comput., vol. C-29, No. 12, Dec. 1980, pp. 1038-1052.
• 23: Rubin, J. and C. H. West, "An improved protocol validation technique," Computer Networks, April 1982.
• 24: 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]
• 25: West, C. H. and P. Zafiropulo, "Automated validation of a communications protocol: The CCITT X.21 recommendations," IBM J. Res. Develop., vol. 22, Jan. 1978, pp. 60-71.
• 26: Yu, Y. T. and M. G. Gouda, "Deadlock detection for a class of communicating finite state machines," IEEE Trans. on Commun., Dec. 1982, pp. 2514-2519.
• 27: Yu, Y. T. and M. G. Gouda, "Unboundedness detection for a class of communicating finite-state machines," Information Processing Letters, Vol. 17, Dec. 1983, pp. 235-240.
• 28: Zafiropulo, P. et al, "Towards analyzing and synthesizing protocols," IEEE Trans. on Commun., vol. COM-28, No. 4, April 1980, pp. 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:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)

General Terms:
Design, Theory