Browse Prior Art Database

Protocol Verification Using Prolog

IP.com Disclosure Number: IPCOM000128009D
Original Publication Date: 1985-Dec-31
Included in the Prior Art Database: 2005-Sep-14
Document File: 13 page(s) / 45K

Publishing Venue

Software Patent Institute

Related People

Deepinder P. Sidhu: AUTHOR [+3]

Abstract

This paper discusses the use of logic programming techniques in the specification, verification, testing and simulation of communication protocols. The protocols are specified using a logic programming language, Prolog. The protocol specifications are formal and directly executable. The advantages of executable specifications are: (1) the specification is itself a prototype of the specified system, (2) incremental development of specifications is possible, (3) behavior exhibited by the specification when executed can be used to check confor-mity of specification with requirements. In the ISO/OSI reference model, the specification of a protocol layer consists of two parts: the specification of the protocol service :interfaces and the specification of entities within the protocol layer. The specification of protocol interfaces forms the standard against which protocols are verified. The input and output of a pro-tocol at a service interface consist of sequences of events occurring at this service interface. These sequences can be compared to those generated from the protocol entity-to-entity interaction to verify a protocol is consistent with its standard. The verification of a protocol with respect to its service interface is possible only if the protocol possesses some desirable properties which include complete-ness, deadlock freeness, boundedness, termination and cyclic behavior. 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 ser-vice interface, the implementation conforms to its standard. The proposed modeling technique has been applied to NBS Class 2 transport layer protocol. Several errors in the specification of connection mangement of the NBS Class 2 transport protocol were discovered, including unspecified receptions, deadlocks and nontermination error indications. Experience with the proposed approach indicates that it is a very powerful method for developing verifiable protocols. 2

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 8% of the total text.

Page 1 of 13

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Protocol Verification Using Prolog

Deepinder P. Sidhu

Department of Computer Science Iowa State University Awes, Iowa 50011

July 1985

TR #85-2'1

July 23, 1985

Protocol Verification Using Prolog Deepinder P. Sidhu Department of Computer Science Iowa State University Ames, Iowa 50011 Key Words: state transition, formal description technique, formal modeling, pro-tocol specification, logic programming, protocol verification, protocol development tools.

Abstract

This paper discusses the use of logic programming techniques in the specification, verification, testing and simulation of communication protocols. The protocols are specified using a logic programming language, Prolog. The protocol specifications are formal and directly executable. The advantages of executable specifications are: (1) the specification is itself a prototype of the specified system, (2) incremental development of specifications is possible, (3) behavior exhibited by the specification when executed can be used to check confor-mity of specification with requirements.

In the ISO/OSI reference model, the specification of a protocol layer consists of two parts: the specification of the protocol service :interfaces and the specification of entities within the protocol layer. The specification of protocol interfaces forms the standard against which protocols are verified. The input and output of a pro-tocol at a service interface consist of sequences of events occurring at this service interface. These sequences can be compared to those generated from the protocol entity-to-entity interaction to verify a protocol is consistent with its standard. The verification of a protocol with respect to its service interface is possible only if the protocol possesses some desirable properties which include complete-ness, deadlock freeness, boundedness, termination and cyclic behavior. 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 ser-vice interface, the implementation conforms to its standard. The proposed modeling technique has been applied to NBS Class 2 transport layer protocol. Several errors in the specification of connection mangement of the NBS Class 2 transport protocol were discovered, including unspecified receptions, deadlocks and nontermination error indications.

Experience with the proposed approach indicates that it is a very powerful method for developing verifiable protocols. 2

1. Introduction

Iowa State University Page 1 Dec 31, 1985

Page 2 of 13

Protocol Verification Using Prolog

Computer communication protocols form the cornerstone upon which distri-buted systems are built. They must be specified precisely and implemented correctly. The International Organization for Standardization (ISO) has developed a...