This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Interactive Protocol Synthesis Algorithm Using a Global State Transition Graph
March 1988 (vol. 14 no. 3)
pp. 394-404

An interactive synthesis algorithm, to construct two communicating finite-state machines (protocols), is presented. The machines exchange messages over two unidirectional FIFO (first-in first-out) channels when the function of the protocol has been given. The synthesis algorithm first constructs the global state transitiion graph (GSTG) of a protoco to be synthesized and then produces the protocol. It is based on a set of production rules and a set of deadlock avoidance rules, which guarantee that complete reception and deadlock freeness capabilities are provided in the interacting process. This synthesis algorithm prevents a designer from creating unspecified reception and nonexecutable transition, avoids the occurrence of deadlocks, and monitors for the presence of buffer overflow.

[1] D. Brand and P. Zafiropulo, "On communicating finite state machines,"J. ACM, vol. 30, no. 2, pp. 323-342, Apr. 1983.
[2] T. P. Blumer and D. P. Sidhu, "Mechanical verfication and automatic implementation of communication protocols,"IEEE Trans. Software Eng., vol. SE-12, pp. 827-843, Aug. 1986.
[3] D. P. Sidhu and T. P. Blumer, "Verification of NBS class 4 transport protocol,"IEEE Trans. Commun., vol. COM-34, pp. 781-789, Aug. 1986.
[4] J. Rubin and C. H. West, "An improved protocol validation technique,"Comput. Networks, vol. 6, pp. 66-73, Apr. 1982.
[5] C. V. Ramamovrthy and S. T. Dong, "Communication protocol synthesis," inProc. COMPSAC 82, Chicago, IL, Oct. 1982, pp. 217- 225.
[6] C. H. West, "General technique for communications protocol validation,"IBM J. Res. Develop., vol. 22, no. 4, pp. 393-404, July 1978.
[7] M. G. Gouda and Y. T. Yu, "Protocol validation by maximal progress state exploration,"IEEE Trans. Commun., vol. COM-32, pp. 94-97, Jan. 1984.
[8] D. P. Sidhu, "Protocol design rules," inProc. Second IFIP Int. Symp. Protocol Specification, Testing, Verification, 1982, pp. 283-300.
[9] M. G. Gouda and Y. T. Yu, "Synthesis of communicating finite state machines with guaranteed progress,"IEEE Trans. Comput., vol. C-32, no. 7, pp. 779-788, 1984.
[10] P. Zafiropouloet al., "Towards analysing and synthesizing protocols,"IEEE Trans. Commun., vol. COM-28, pp. 655-660, Apr. 1980.
[11] N. Shiratoriet al., "EXPA: Validation method of a communication protocol based on the perturbation analysis,"Trans. IPS Japan, vol. 26, No. 3, pp. 446-453, 1985.
[12] T. Higashinoet al., "An algebraic specification of HDLC procedures and its verification,"IEEE Trans. Software Eng., vol. SE-10, pp. 825-836, Nov. 1984.
[13] B. T. Hailpern, "A simple protocol whose proof isn't,"IEEE Trans. Commun., vol. COM-33, pp. 330-337, Apr. 1985.
[14] B. Hailpern and S. Owicki, "Modular verification of computer communication protocols,"IEEE Trans. Comm., vol. COM-31, Jan. 1983.
[15] S. S. Lam and A. U. Shankar, "Protocol verification via projections,"IEEE Trans. Software Eng., vol. SE-8, pp. 460-489, Sept. 1982.
[16] R. L. Schwartz and P. M. Melliar-Smith, "From state machines to temporal logic: specification methods for protocol standards,"IEEE Trans. Commun., vol. COM-30, pp. 2486-2496, Dec. 1982.
[17] Proc. Sixth IFIP Int. Workshop Protocol Specification, Testing, Verification, June 1986.
[18] Proc. Fifth IFIP Int. Workshop Protocol Specification, Testing, Verification, June 1985.
[19] A. Tannenbaum,Computer Networks. Englewood Cliffs, NJ: Prentice-Hall, 1981.
[20] X. Y. Zhang, "A study on protocol synthesis," M.E. thesis, Dep. Elec. Commun. Eng., Tohoku Univ., Sendai, Japan, Jan. 1986.

Index Terms:
interactive protocol synthesis algorithm; global state transition graph; finite-state machines; global state transition graph; production rules; deadlock avoidance rules; complete reception; deadlock freeness; buffer overflow; finite automata; graph theory; interactive programming; protocols
Citation:
Y.X. Zhang, K. Takahashi, N. Shiratori, S. Noguchi, "An Interactive Protocol Synthesis Algorithm Using a Global State Transition Graph," IEEE Transactions on Software Engineering, vol. 14, no. 3, pp. 394-404, March 1988, doi:10.1109/32.4659
Usage of this product signifies your acceptance of the Terms of Use.