Dismiss
InnovationQ will be updated on Sunday, Oct. 22, from 10am ET - noon. You may experience brief service interruptions during that time.
Browse Prior Art Database

Formal Modeling of Communication Protocols

IP.com Disclosure Number: IPCOM000128662D
Original Publication Date: 1981-Dec-31
Included in the Prior Art Database: 2005-Sep-16
Document File: 18 page(s) / 60K

Publishing Venue

Software Patent Institute

Related People

Carl A. Sunshine: AUTHOR [+3]

Abstract

. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2. MEANING OF SPECIFICATION AND VERIFICATION 3. SPECIFICATION METHODS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Finite State Automata ............................................................... Abstract Machine Model ............................................................ Formal Languages . . . . . . Sequencing Expressions ........................ Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . Buffer Histories ..... Abstract Data Types . . . . . . . . . . . . . . . . . . . . . . Programs and Program Assertions . . . . . . . . . . . . . . . 4. VERIFICATION . . . . . . State Exploration . . . . Symbolic Execution. . Structural Induction ............................................................... Program Verification............................................................... 3 4 5 7 9 JO ......... 12 13

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

Page 1 of 18

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Formal Modeling of Communication Protocols

Carl A. Sunshine

ISLIRR-81-89 March 1981 INFORMATION SCIENCES INSTITUTE

4676 Admiralty WaylMarina del ReylCali f ornia 90291 UNIVERSITY OF SOUTHERN CALIFORNIA ~~ (213) 822-1511

This research is supported by the Defense Advanced Research Projects Agency under Contract No. DAHC15 72 C OCi08. Views and conclusions contained in this report are the author's and should not 'be interpreted as representing the official opinion or policy of DARPA, the U.S. Government, or any person or agency connected with them.

This document is approved for public release and sale; distribution is unlimited.

CONTENTS

1. INTRODUCTION . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2. MEANING OF SPECIFICATION
AND VERIFICATION

3. SPECIFICATION METHODS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . Finite State Automata ............................................................... Abstract Machine Model
............................................................ Formal Languages . . . . . . Sequencing Expressions
........................ Petri Nets . . . . . . . . . . . . . . . . . . . . . . . . . Buffer Histories ..... Abstract Data
Types . . . . . . . . . . . . . . . . . . . . . . Programs and Program Assertions . . . . . . . . . . . . . . .

4. VERIFICATION . . . . . . State Exploration . . . . Symbolic Execution. . Structural Induction
............................................................... Program
Verification...............................................................

3 4 5 7 9 JO ......... 12 15 Design Rules 5. CONCLUSIONS. REFERENCES.

16 16 18 19 20 20

FIGURES

Figure 2.1. User view of protocol layer . . . . . . . . Figure 2.2. Internal structure of protocol layer .
F igure 3.1. Finite State Automata for connection establishment . . . . . . . . . . . . . . . . . . . . . . . . . .
. . Figure 3.2. Protocol service in Special . . . . . . . . . . . . . . . . . . . . . . . . . . . Figure 3.3.
Alternating bit protocol in formal grammar . . . . . . . . . . . . . Figure 3.4. CCITT X.25 as protocol
sequence expression . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Figure 3.5. Alternating bit
protocol as a Petri Net . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Figure 3.6. Protocol
service in Gypsy ................................................... Figure 3.7. Protocol service in AFFIRM . . . . .
. . . . . . . . Figure 3.8. Alternating bit protocol in state deltas . . . . . .

10 11 12 14 17

University of Southern California Page 1 Dec 31, 1981

Page 2 of 18

Formal Modeling of Communication Protocols

1. INTRODUCTION

As computer networks proliferate, the design of properly functioning communication procedures or protocols becomes ever more important. Traditional methods of informal narrative specifications and ad hoc vali...