Browse Prior Art Database

Protocol Verification Using Prolog

IP.com Disclosure Number: IPCOM000148440D
Original Publication Date: 1985-Jul-31
Included in the Prior Art Database: 2007-Mar-29
Document File: 22 page(s) / 1M

Publishing Venue

Software Patent Institute

Related People

Sidhu, Deppinder P.: AUTHOR [+2]

Abstract

Deepinder P. Sidhu

This text was extracted from a PDF file.
At least one non-text object (such as an image or picture) has been suppressed.
This is the abbreviated version, containing approximately 8% of the total text.

Page 1 of 22

Protocol Verification Using Prolog

Deepinder P. Sidhu

Department of Computer Science Iowa State University

Ames , Iowa 5001 1

July 1985

[This page contains 1 picture or other non-text object]

Page 2 of 22

July 23, 1985

Protocol Verification Using Prolog

Deepinder P. Sidhu

Department of Computer Science Iowa State University

Ames, Iowa 5001 1

Key Words: state transition, formal description technique, formal modeling, pro- tocol specification, logic programming, protocol verification. protocol development tools.

[This page contains 1 picture or other non-text object]

Page 3 of 22

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: (I) the specifica1,ion 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 verjfication 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, term ination and cyclic behavior.

   When a prolocol has been implemented, the correctness of its implernentation 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 nonterrnination error indications.

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

[This page contains 1 picture or other non-text object]

Page 4 of 22

1. Introduction

   Computer communication protocols form the cornerstone up...