Modeling physical layer protocols using communicating finite state machines

ABSTRACT

We illustrate the usefulness of communicating finite state machines in modeling a number of physical layer protocols that include (i) an asynchronous start-stop protocol and (ii) a protocol for synchronous transmission with modems. Each protocol is modeled as a network of four finite state machines that communicate by exchanging messages over unbounded, FIFO channels. (Two machines are used to model the protocol itself, while the other two are used to model its interface to the upper data link protocol in the protocol hierarchy.) We outline a methodology to verify communication boundedness and progress for each protocol model. The methodology is based on three techniques that were proposed earlier to verify networks of communicating finite state machines; they are network decomposition, machine equivalence, and closed covers.

REFERENCES

• 1: H. V. Bertine, "Physical interfaces and protocols," in Computer Network Architectures and Protocols, P. E. Green, Ed. New York: Plenum ~'ress, 1982, pp. 57-83.
• 2: G. V. Bochmann, "Finite state description of communication protocols," Comput. Networks, vol. 2, pp. 361-371, 1978.
• 3: G. V. Boehmann and C. Sunshine, "Formal methods in communication protocol design," IEEE Trans. Commun., vol. COM-28, pp.624-631, Apr. 1980.
• 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: 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
• 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: R. J. Cyper, Communications Architecture for Distributed Systems, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1978
• 8: M. G. Gouda, "Closed covers: to verify progress for communicating finite state machines," IEEE Trans. Software Eng., vol. SE-10, pp. 840-855, Nov. 1984.
• 9: M. G. Gouda and K. S. The, "On modeling and verification of physical layer protocols," Tech. Rep., Dep. Comput. Sci., Univ. Texas, Austin, TX, in preparation.
• 10: M. G. Gouda, K. S. The, and C. K. Chang, "Verification of distributed synchronization systems via deeomposltion," Teeh. Rep., Dep. Comput. Sci., Univ. Texas, Austin, TX, in preparation.
• 11: Mohamed G. Gouda , C. H. Youn, On the Notion of Equivalence for Communicating Finite State Machines, University of Texas at Austin, Austin, TX, 1984
• 12: B. T. Hailpern and S. S. Owicki, "Modular verification of computer communication protocols," IEEE Trans. Commun., vol. COM-31, pp. 56-68, Jan. 1983.
• 13: S. S. Lain and A. U. Shankar, "Protocol verification via projections," IEEE Trans. Software Eng., vol. SE-10, pp.325-342, July 1984.
• 14: John E. McNamara, Technical aspects of data communication (3rd ed.), Digital Press, Newton, MA, 1988
• 15: A. S. Tanenbaum, Computer networks, Prentice-Hall, Inc., Upper Saddle River, NJ, 1988
• 16: K. S. The, "A framework for formal modeling and verification of physical layer protocols," Master's thesis, Univ. Texas, Austin, TX, 1985.
• 17: P. Zafiropulo, C. H. West, H. Rudin, D. Brand, and D. Cowan, "Towards analyzing and synthesizing protocols," IEEE Trans. Commun., vol. COM-28, pp. 651-661, Apr. 1980.

INDEX TERMS

Primary Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES

General Terms:
Design, Theory