Browse Prior Art Database

Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models

IP.com Disclosure Number: IPCOM000128661D
Original Publication Date: 1981-Dec-31
Included in the Prior Art Database: 2005-Sep-16

Publishing Venue

Software Patent Institute

Related People

David H. Thompson: AUTHOR [+7]

Abstract

. . . . . . . . . . . . . . . . . . . . . . ... . .

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

Page 1 of 42

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models

David H. Thompson Carl A. Sunshine Roddy W. Erickson Susan L. Gerhart Daniel Schwabe

CONTENTS

1. INTRODUCTION . . . . . . . . . . . . . . . . . . . . . . ... . .

1.1. State Transition Models . . . . . . . . . . . . . . . . . . . . . . . . . . .

1.2. Specification and Verification in Affirm . . . . . . . . . . . . .

1.2.1. Data Abstraction . . . . ,

1.2.2. Theorem Proving . . . . ,

1.3. Protocols . . . . . . . . . . . . . . ,

1.3.1. Protocol Specification

1.3.2. Protocol Verification. ,

1.4. Related Work . . . . . . . . . . . , 2. AN OVERVIEW OF OUR METHOD OF PROTOCOL
SPECIFICATION AND VERIFICATION . . . . .

3. A SERVICE SPECIFICATION FOR A SIMPLE MESSAGE SYSTEM . . . . . . . . . . . . . . . . . . . .
. . , . .

3.1. State Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3.2. State Transitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

3.3. Behavior of the Simple Message System . . . . . . . . . . .

3.4. Converting State Transition Specifications to Affirm

3.4.1. State Transition Function -> Constructor . . . . . . . . . . . . . . .

3.4.2. State Variable - Selector . . . . . . . . . . . . . . . . . . . . . . . . . .

3.4.3. Transition Definition -> Set of Axioms

3.5. The Affirm Representation...

3.6. Properties of a Specification

University of Southern California Page 1 Dec 31, 1981

Page 2 of 42

Specification and Verification of Communication Protocols in AFFIRM Using State Transition Models

3.7. Alternative Notations . . . . . . . . . . . . . . . . . . . . . . . . .

4. VERIFICATION ISSUES . . . . . . . . . . 8 9

4.1. Verifying Properties-of a Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. , 19

4.2. Verifying the Protocol against the Service Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 20

4.3. Verifying a Program against the Protocol Specification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
22 5. DETAILED EXAMPLE: THE ALTERNATING BIT PROTOCOL 5.1. A Brief Description of the Protocol . . . . . . . . . . . . . . . . . . . . . . . . 5.2. A State Transition Machine for the Alternating Bit
Protocol . . 5.2.1. Data Types Used in the Specification . . . . . . . . . . . . . . . . . 5.2.2. State
Variables . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2.3. State Transition Functions . . . . . . . . .
. . . . . . . . . . . . . . . . . 5.3. The Affirm Representation . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.4.
Verifying the Protocol against the Service Specification . . . . . . 5.4.1. Safety
......................................... 5.4.2. Liveness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.5.
Protocol Properties and Invariants . . . . . . . . . . . . . . . . . . . . . 5.6. Impl...