Browse Prior Art Database

Formal Techniques for Protocol Specification and Verification

IP.com Disclosure Number: IPCOM000131444D
Original Publication Date: 1979-Sep-01
Included in the Prior Art Database: 2005-Nov-11
Document File: 12 page(s) / 43K

Publishing Venue

Software Patent Institute

Related People

Carl Sunshine: AUTHOR [+3]

Abstract

This article describes some of the more formal techniques which have been brought to bear on this requirement. We focus on two key problem areas -- protocol specification and verification of logical correctness. Methods for analyzing the efficiency of protocols have been discussed elsewhere.'

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

Page 1 of 12

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

This record contains textual material that is copyright ©; 1979 by the Institute of Electrical and Electronics Engineers, Inc. All rights reserved. Contact the IEEE Computer Society http://www.computer.org/ (714-821-8380) for copies of the complete work that was the source of this textual material and for all use beyond that as a record from the SPI Database.

Formal Techniques for Protocol Specification and Verification

Carl Sunshine

The Rand Corporation

(Image Omitted: Certain formal approaches, such as transition techniques and reachability analysis, show promising results when applied to protocol specification and verification.)

Communication protocols play an important role in computer networks and distributed systems. The increasing variety and complexity of such protocols demand more powerful techniques to produce successful systems. This article describes some of the more formal techniques which have been brought to bear on this requirement. We focus on two key problem areas -- protocol specification and verification of logical correctness. Methods for analyzing the efficiency of protocols have been discussed elsewhere.'

As protocols are developed, designers must provide descriptions of them for many purposes. Initial descriptions provide a central frame of reference allowing cooperation among designers of different parts of a protocol system. Descriptions also play a role in the verification process. The design must be checked for logical correctness. Then the protocol must be implemented, and if it is in wide use, many different implementations may have to be checked for compliance with a standard. Although narrative descriptions and informal walk-throughs are invaluable elements of this process, painful experience has shown that by themselves they are inadequate to handle all but the simplest protocols.

A great deal of confusion surrounds the words "specification" and "verification" as they apply to computer communication protocols. Hence our first goal will be the definition of these concepts in the context of a layered model of protocols. Next, an overview of various approaches emphasizes the use of more formal specification and verification. techniques. We conclude by reviewing some recent applications of these techniques, and suggesting some directions for future work.

A protocol system model

From the user's point of view, a protocol provides a certain set of services allowing interaction of various sorts with other users. (We will restrict our consideration to interactions between a pair of users, although most of the concepts are applicable to multi-user protocols.) Different protocols provide different services, such as general data transfer or terminal support. The user is concerned with the nature of the service, but not with how the protocol manages to provide it. Hence we may view the protocol as a "black box" (Figure 1) whose service is fully de...