To correct communicating finite state machines

ABSTRACT

A number of methods have been proposed to validate the communication between processes which exchange messages through bounded FIFO channels. However design criteria and rules are developed to construct correct protocols. In this paper, our objective is to propose a new correcting method for a pair of communicating finite state machines and we ensure that the communication is perfect and progresses indefinitely i.e deadlock-free, liveness, bounded, and without noexecutable transitions, unspecified receptions. The time complexity is bounded by O(nm) where n is the number of states and m is the number of transitions of a given machine. The first method is defined by adding receiving transitions and in the second we complete our results by adding sending transitions , then we obtain symmetric and isomorphic machines with unbounded communication.

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: G. Bochmann "Finite state descriptions of communication protocols", Computer networks, pp 361-372, october 1978.
• 3: G. Bochmann, M. Merlin "On the construction communication protocols", Proc. 5 thlnt. Conf. Comp.com., Atlanta, GA, Edt. North-Holland pp 371-378,1980.
• 4: 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]
• 5: Siyi Terry Dong, The modeling, analysis and synthesis of communication protocols, 1983
• 6: M. G. Gouda , C. K. Chang, A technique for proving liveness of communicating finite state machines with examples, Proceedings of the third annual ACM symposium on Principles of distributed computing, p.38-49, August 27-29, 1984, Vancouver, British Columbia, Canada [doi>10.1145/800222.806734]
• 7: M. Gouda, Y. Yu " Synthesis of communicating finite-state machines with guaranteed progress", trans. Cornmun., vol. COM-32, pp 779-788, July 1984.
• 8: H. Mountassir, R. Sijelmassi "Formulation syntaxique la communication de processus asynchrones a travers des canaux FIFO", A paraitre dans Rairo,1988.
• 9: H. Mountassir" Correction lintaire de protocoles communication", Rapp. interne, Universit6 de Juillet 88 soumis a publication.
• 10: H. Mountassir" On basic rewriting rules communicating machines", symposium on future distributed computing systems (DCCS'90), Hong-Kong (sept. 1988).
• 11: C. Jard, M. Raynal "De la nectssit6 de la sptcification proprittts pour des algorithmes distributs" Rapp. IRISA de Rennes, 1986.
• 12: Deepinder P. Sidhu, Rules for synthesizing correct communication protocols, ACM SIGCOMM Computer Communication Review, v.12 n.1, p.35-51, January 1982 [doi>10.1145/1040119.1040122]
• 13: C. West et al. "A general technique for commmnication control validation", IBM J. Res. Develop. vol July 1978.
• 14: P. Zafiropulo et al. "Towards analyzing and synthesizing protocols", IEEE transactions on communication, vol COM 28, pp 651-661, april 1980.

INDEX TERMS

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

Additional Classification:
  C. Computer Systems Organization
  C.2 COMPUTER-COMMUNICATION NETWORKS
      C.2.1 Network Architecture and Design
          Subjects: Store and forward networks

  D. Software
  D.4 OPERATING SYSTEMS
      D.4.4 Communications Management
          Subjects: Message sending

General Terms:
Algorithms, Design, Verification