This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Formal Methods for Protocol Testing: A Detailed Study
April 1989 (vol. 15 no. 4)
pp. 413-426

The authors present a detailed study of four formal methods (T-, U-, D-, and W-methods) for generating test sequences for protocols. Applications of these methods to the NBS Class 4 Transport Protocol are discussed. An estimation of fault coverage of four protocol-test-sequence generation techniques using Monte Carlo simulation is also presented. The ability of a test sequence to decide whether a protocol implementation conforms to its specification heavily relies on the range of faults that it can capture. Conformance is defined at two levels, namely, weak and strong conformance. This study shows that a test sequence produced by T-method has a poor fault detection capability, whereas test sequences produced by U-, D-, and W-methods have comparable (superior to that for T-method) fault coverage on several classes of randomly generated machines used in this study. Also, some problems with a straightforward application of the four protocol-test-sequence generation methods to real-world communication protocols are pointed out.

[1] H. Zimmermann, "OSI reference model--The ISO model of architecture for Open Systems Interconnection,"IEEE Trans. Commun., vol. COM-28, no. 4, pp. 425-432, Apr. 1980.
[2] R. J. Linn and W. H. McCoy, "Producing tests for implementations of OSI protocols," inProtocol Specification, Testing, and Verification III, H. Rudin and C. H. West, Eds. Amsterdam. The Netherlands: North-Holland, 1983, pp. 505-520.
[3] D. P. Sidhu, "Protocol verification via executable logic specifications," inProtocol Specification, Testing, and Verification III, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: North-Holland. 1983, pp. 237-248.
[4] D. P. Sidhu and C. S. Crall, "Executable logic specifications for protocol service interfaces,"IEEE Trans. Software Eng., vol. 14, Jan. 1988.
[5] D. Rayner, "Standardizing conformance testing for OSI," inProtocol Specification, Testing, and Verification, V. M. Diaz, Ed. Amsterdam, The Netherlands: North-Holland, 1986.
[6] D. P. Sidhu, "Protocol verification using prolog," ISU Preprint, 1985.
[7] S. Naito and M. Tsunoyama, "Fault detection for sequential machines by transition tours," inProc. IEEE Fault Tolerant Comput. Conf., 1981.
[8] K. Sabnani and A. Dahbura, "A protocol test generation procedure,"Comput. Networks ISDN Syst., North-Holland, no. 15, pp. 285-297, 1988.
[9] A. Aho, J. Hopcroft, and J. Ullman,Data Structures and Algorithms. Reading, MA: Addison-Wesley, 1983.
[10] G. Gonenc, "A method for the design of fault detection experiments,"IEEE Trans. Comput., vol. C-19, pp. 551-558, June 1970.
[11] Z. Kohavi,Switching and Finite Automata Theory, New York: McGraw-Hill, 1978.
[12] T. Chow, "Testing software design modeled by finite-state machines,"IEEE Trans. Software Eng., vol. SE-4, pp. 178-187, Mar. 1978.
[13] B. W. Kernighan and D. M. Ritchie,The C Programming Language. Englewood Cliffs, NJ: Prentice-Hall, 1978.
[14] A. D. Friedman and P. R. Menon,Fault Detection in Digital Circuits. Englewood Cliffs, NJ: Prentice-Hall, 1971.
[15] M. A. Harrison, "On asymptotic estimates in switching theory and automata theory,"J. ACM, vol. 13, pp. 151-157, 1966.
[16] W. Cheney and D. Kincaid,Numerical Mathematics and Computing, Monterey CA: Brooks/Cole, 1980.
[17] "Specification of a transport protocol for computer communications, Volume I: Overview and services," Nat. Bureau Standards, Washington, DC, Rep. ICST/HLNP-83-1, Jan. 1983.
[18] "Specification of a transport protocol for computer communications, Volume 3: Class 4 protocol," Nat. Bureau Standards, Washington. DC, Rep. ICST/HLNP-83-1, Jan. 1983.
[19] "Specification of a transport protocol for computer communication, Volume 4: Service specifications," Nat. Bureau Standards, Washington, DC, Rep. ICST/HLNP-83-4, Jan. 1983.
[20] 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.
[21] B. Sarikaya and G.v. Bochmann, "Synchronization and specification issues in protocol testing,"IEEE Trans. Commun., vol. COM-32, pp. 389-395, Apr. 1984.
[22] M. U. Uyar and A. T. Dahbura, "Optimal test sequence generation for protocols: The Chinese postman algorithm applied to Q.931," inProc. IEEE Global Telecommun., Conf., 1986.
[23] A. Dahbura and K. Sabnani, "Experience in estimating fault coverage of a protocol test," inProc. IEEE INFOCOM'88, 1988, pp. 71- 79.
[24] A. V. Aho, J. E. Hopcroft, and J. D. Ullman,The Design and Analysis of Computer Algorithms. Menlo Park, CA: Addison-Wesley, 1974.
[25] D. P. Sidhu and T. K. Leung, "Experience with test generation for real protocols," inProc. SIGCOMM '88 Symp.: Communication Architectures and Protocols, 1988, pp. 257-261.
[26] D. P. Sidhu and T. K. Leung, "Formal methods for protocol testing--A detailed study," ISU Preprint, Tech. Rep. 86-23, 1986.

Index Terms:
protocol testing; test sequences; NBS Class 4 Transport Protocol; fault coverage; protocol-test-sequence generation techniques; Monte Carlo simulation; protocol implementation; fault detection; fault coverage; real-world communication protocols; conformance testing; failure analysis; Monte Carlo methods; protocols.
Citation:
D.P. Sidhu, T.K. Leung, "Formal Methods for Protocol Testing: A Detailed Study," IEEE Transactions on Software Engineering, vol. 15, no. 4, pp. 413-426, April 1989, doi:10.1109/32.16602
Usage of this product signifies your acceptance of the Terms of Use.