A technique for proving liveness of communicating finite state machines with examples

ABSTRACT

Consider a network of communicating finite state machines that exchange messages over unbounded, FIFO channels. Each machine in this network has a finite number of states (called nodes), and state transitions (called edges), and can be defined by a labelled directed graph. A node in one of the machines is said to be “live” iff it is reached by its machine infinitely often during the course of communication, provided that the machines behave in some “fair” fashion. We discuss a technique to verify that a given node is live in such a network. This technique can be automated, and is effective even if the network under consideration is unbounded (i.e. has an infinite number of reachable states). We use our technique to establish the liveness of three distributed solutions to the mutual exclusion problem.

REFERENCES

• 1: 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]
• 2: Bochmann, G.V., "Finite state description of communication protocols," Computer Networks, Vol. 2, 1978, pp. 361-371.
• 3: Bochmann, G. V. and C. Sunshine, "Formal methods in communication protocol design," IEEE Trans. on Commun., April 1980, pp.624-631.
• 4: Chandy, K. M. and J. Misra, "The drinking philosophers problem," TR LCS-8402, Dept. of Computer Sciences, Univ. of Texas at Austin, Feb. 1984.
• 5: Chang, C.K., M.G. Gouda, and L.E. Rosier, "Deciding liveness for special classes of communicating finite state machines," In preparation.
• 6: Chang, C. K, "Proving liveness properties for communicating machines," Ph.D. Thesis, Univ. of Texas at Austin, In preparation.
• 7: 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
• 8: E. W. Dijkstra, Solution of a problem in concurrent programming control, Communications of the ACM, v.8 n.9, p.569, Sept. 1965 [doi>10.1145/365559.365617]
• 9: Mohamed G. Gouda, Closed Covers: to Verify Progress for Communicating Finite State Machines, University of Texas at Austin, Austin, TX, 1982
• 10: Mohamed G. Gouda , C. K. Chang, Proving Liveness for Networks of Communicating Finite State Machines, University of Texas at Austin, Austin, TX, 1984
• 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: Gouda, M.G. and Y.T. Yu, "Protocol validation by maximal progress state exploration," IEEE Trans. on Commun., Vol. COM-32. No. 1, Jan. 1984, pp. 94-97.
• 13: Gouda, M. G. and Y. T. Yu, "Synthesis of communicating finite state machines with guaranteed progress", TR-179, Dept. of Computer Sciences, Univ. of Texas at Austin, June 1981. Revised Jan. 1983. Revised Oct. 1983. To appear in IEEE Trans. on Commun., July 1984.
• 14: Hailpern, B. T. and S. S. Owicki, "Modular verification of computer communication protocols," IEEE Trans. on Commun., Vol. COM-31, No. 1, Jan. 1983, pp. 56-68.
• 15: Donald E. Knuth, Additional comments on a problem in concurrent programming control, Communications of the ACM, v.9 n.5, p.321-322, May 1966 [doi>10.1145/355592.365595]
• 16: Misra, J. and K. M. Chandy, "Proof of networks of processes," IEEE Tran. on Software Eng., Vol. SE-7, No. 4, July 1981.
• 17: 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]
• 18: Susan Owicki , Leslie Lamport, Proving Liveness Properties of Concurrent Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.455-495, July 1982 [doi>10.1145/357172.357178]
• 19: Pnueli, A., "The temporal semantics of concurrent programs," Theoretical Computer Science, Vol. 13, 1981, pp. 45-60.
• 20: Louis E. Rosier , Mohamed G. Gouda, On Deciding Progress for a Class of Communication Protocols, University of Texas at Austin, Austin, TX, 1983
• 21: 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.
• 22: 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.
• 23: Zafiropulo, P., C.H. West, H. Rudin, D. Brand, and D. Cowan, "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.1 Network Architecture and Design
          Subjects: Network communications

Additional Classification:
  B. Hardware
  B.4 INPUT/OUTPUT AND DATA COMMUNICATIONS
      B.4.2 Input/Output Devices
          Subjects: Channels and controllers

  D. Software
  D.4 OPERATING SYSTEMS
      D.4.1 Process Management
          Subjects: Mutual exclusion

  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, Management, Theory