This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Executable logic specifications for protocol service interfaces
January 1988 (vol. 14 no. 1)
pp. 98-121

A general, formal modeling technique for protocol service interfaces is discussed. An executable description of the model using a logic-programming-based language, Prolog, is presented. The specification of protocol layers consists of two parts, the specification of the protocol interfaces and the specification of entities within the protocol layer. The specification of protocol interfaces forms the standard against which protocols are verified. When a protocol has been implemented, the correctness of its implementation can be tested using the sequences of events generated at the service interface. If the behavior of the protocol implementation is consistent with the behavior at the service interface, the implementation conforms to its standard. To illustrate how it works, the model is applied to the service interfaces of protocol standards developed for the transport layer of the ISO/OSI architecture. The results indicate that Prolog is a very useful formal language for specifying protocol interfaces.

[1] 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.
[2] G. Bochmann, "A general transition model for protocols and communication services,"IEEE Trans. Commun., vol. 28, pp. 643-650, 1980.
[3] G. V. Bochmann and C. A. Sunshine, "Formal methods in communication protocol design,"IEEE Trans. Commun., vol. COM-28, no. 4, pp. 624-631, Apr. 1980.
[4] F. Clocksin and S. Mellish,Programming in Prolog. Berlin: Springer Verlag, 1981.
[5] H. C. Folts, "Scanning the issue,"Proc. IEEE, vol. 71, no. 12, pp. 1331-1333, Dec. 1983.
[6] R. Kowalski, "Algorithm = Logic + Control,"Comm. ACM, Vol. 22, No. 7, July 1979, pp. 424-436.
[7] P. F. Linington, "Fundamentals of the layer service definitions and protocol specifications,"Proc. IEEE, vol. 71, no. 12, pp. 1341-1345, Dec. 1983.
[8] R. J. Linn and W. H. McCoy, "Producing tests for implementations of OSI Protocols," inProrocol. Specification, Testing, and verfication. III, H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: North-Holland, 1983, pp. 505-520.
[9] L. Logrippo, D. Simon, and H. Ural, "Esecutable description of the OSI transport service in prolog," inProtocol Specification, Testing and Verfication, IV, Y. Yemini, R. Strom, and S. Yemini, Eds. Amsterdam, The Netherlands: North-Holland, 1985, pp. 279-293.
[10] "Military standard transmission control protocol," Dep. Defense, Washington, DC, Rep. MIL-STD-1778. Aug. 12, 1983.
[11] F. Pereira, Ed.C-Prolog User's Manual, Version 1.5, 1984.
[12] B. Sarikaya and G.v. Bochmann, "Synchronization and specification issues in protocol testing,"IEEE Trans. Commun., vol. COM-32, pp. 389-395, Apr. 1984.
[13] D. P. Sidhu, "Protocol verification via executable logic specifications," inProtocol Specification, Testing, and Verfication, III. H. Rudin and C. H. West, Eds. Amsterdam, The Netherlands: North-Holland, 1983, pp. 237-248.
[14] D. P. Sidhu and T. P. Blumer, "An automated protocol development system," inIEEE 1983 Symp. Application and Assessment of Automated Tools for Software Development, 1983, pp. 10-23.
[15] "Specification of a transport protocol for computer communications. volume I: Overview and services," Nat. Bureau Standards. Washington, D.C., Rep. ICST/HLNP-83-1, Jan. 1983.
[16] "Specification of a transport protocol for computer communication, volume 4: Service specifications," Nat. Bureau Standards. Washington, D.C., Rep. ICST/HLNP-83-4, Jan. 1983.
[17] 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.

Index Terms:
executable logic specifications; protocol service interfaces; formal modeling technique; logic-programming-based language; Prolog; protocol layers; correctness; protocol standards; transport layer; ISO/OSI; formal language; formal languages; PROLOG; protocols; specification languages
Citation:
D.P. Sidhu, C.S. Crall, "Executable logic specifications for protocol service interfaces," IEEE Transactions on Software Engineering, vol. 14, no. 1, pp. 98-121, Jan. 1988, doi:10.1109/32.4626
Usage of this product signifies your acceptance of the Terms of Use.