This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Acyclic Expansion Algorithm for Fast Protocol Validation
August 1988 (vol. 14 no. 8)
pp. 1059-1070

For the development of communications software composed of many modules, protocol validation is considered essential to detect errors in the interactions among the modules. Protocol validation techniques previously proposed have required validation time that is too long for many actual protocols. The authors propose a novel fast protocol validation technique to overcome this drawback. The proposed technique is to construct the minimum acyclic form of state transitions in individual processes of the protocol, and to detect protocol errors such as system deadlocks and channel overflows fast. The authors also present a protocol validation system based on the technique to confirm its feasibility and show validation results for some actual protocols. As a result, the protocol validation system is expected to improve productivity in the development and maintenance of communications software.

[1] R. Balzer, T. E. Cheatham, Jr., and C. Green, "Software technology in the 1990's: Using a new paradigm,"Computer, vol. 16, no. 11, pp. 39-45, Nov. 1983.
[2] D. Brand and P. Zafiropulo, "On communicating finite state machines,"J. ACM, vol. 30, no. 2, pp. 323-342, Apr. 1983.
[3] 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.
[4] Y. Kakuda, Y. Wakahara, M. Norigoe, and T. Oda, "Protocol validation by acyclic expansion of state transitions in individual processes," IECE Japan, Tech. Group Paper SE-83-168, Mar. 1984 (in Japanese).
[5] Y. Kakuda, Y. Wakahara, and M. Norigoe, "Protocol validation for protocols with buffers of bounded capacity--NP-completeness and a validation algorithm," IECE Japan, Tech. Group Paper EC84-14, June 1984 (in Japanese).
[6] Y. Kakuda, Y. Wakahara, and M. Norigoe, "Communication protocol validation for protocols with unbounded overflow," IECE Japan, Tech. Group Paper EC84-65, Feb. 1985 (in Japanese).
[7] Y. Kakuda, Y. Wakahara, and M. Norigoe, "Structured validation of protocol specifications," IECE Japan. Tech. Group Paper IN86-20, June 1986 (in Japanese).
[8] S. T. Vuong and D. D. Cowan, "Reachability analysis of protocols with FIFO channels," inACM SIGCOMM Symp. '83: Communications Architecture and Protocols, 1983, pp. 49-57.
[9] C. H. West, "General technique for communications protocol validation,"IBM J. Res. Develop., vol. 22, no. 4, pp. 394-404, July 1978.
[10] Y. T. Yu and M. G. Gouda, "Unboundedness detection for a class of communicating finite-state machines,"Inform. Processing Lett., vol. 17, pp. 235-240, Dec. 1983.

Index Terms:
finite state machines; acyclic expansion algorithm; protocol validation; communications software; state transitions; protocol errors; system deadlocks; channel overflows; computer communications software; finite automata; program verification; protocols; system recovery
Citation:
Y. Kakuda, Y. Wakahara, M. Norigoe, "An Acyclic Expansion Algorithm for Fast Protocol Validation," IEEE Transactions on Software Engineering, vol. 14, no. 8, pp. 1059-1070, Aug. 1988, doi:10.1109/32.7616
Usage of this product signifies your acceptance of the Terms of Use.