Automated Protocol Verification.

Abstract

Four general-purpose automated verification systems (Affirm, Formal Development Methodology (Ina Jo), Gypsy, and Concurrent State Deltas) were applied to computer network protocols in order to evaluate the ability of such systems to provide significant results in formal protocol specification and verification. Each system had a particular strength: Affirm was most polished and flexible; FDM supported abstract machine specifications directly; Gypsy supported stateless I/O (Input/Output) history type specifications; CSD supported more automatic proof and timing properties. However, none of the systems had all necessary features or was powerful enough to fully handle complex protocols. The relative strengths of the systems are compared, detailed examples of their use are presented, and suggestions for further work are given. (Author)

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Oct 01, 1982
Accession Number
ADA126271

Entities

People

  • Carl A. Sunshine
  • David A. Smallberg

Organizations

  • University of Southern California

Tags

Communities of Interest

  • Advanced Electronics

DTIC Thesaurus Topics

  • Abstracts
  • Classification
  • Complex Systems
  • Computer Communications
  • Computer Networks
  • Computers
  • Data Transmission
  • Digital Communications
  • Hierarchies
  • Hypotheses
  • Information Science
  • Language
  • Network Protocols
  • Networks
  • Robotics
  • Security
  • Software Development

Fields of Study

  • Computer science

Readers

  • Computer Networking
  • Computer Science.
  • Systems Analysis and Design