Formal Methods for Communication Protocol Specification and Verification

Carl A. Sunshine

Published 1979

Increasingly numerous and complex communication protocols are being employed in distributed systems and computer networks of all types. This Note describes some of the more formal techniques that are being developed to facilitate design of correct protocols. Our major conclusion is that it is vital to specify the services provided by a protocol layer in addition to specifying the cooperating protocol entities which make up the layer. We develop service specifications of several representative protocols by using formal techniques from software engineering such as abstract machines and buffer histories. A survey of protocol verification methods and a bibliography indexed by key phrases are also provided.

Topics

Document Details

  • Availability: Web Only
  • Year: 1979
  • Pages: 102
  • Document Number: N-1429-ARPA/NBS

Citation

Chicago Manual of Style

Sunshine, Carl A., Formal Methods for Communication Protocol Specification and Verification. Santa Monica, CA: RAND Corporation, 1979. https://www.rand.org/pubs/notes/N1429.html.
BibTeX RIS

This publication is part of the RAND note series. The note was a product of RAND from 1979 to 1993 that reported miscellaneous outputs of sponsored research for general distribution.

This document and trademark(s) contained herein are protected by law. This representation of RAND intellectual property is provided for noncommercial use only. Unauthorized posting of this publication online is prohibited; linking directly to this product page is encouraged. Permission is required from RAND to reproduce, or reuse in another form, any of its research documents for commercial purposes. For information on reprint and reuse permissions, please visit www.rand.org/pubs/permissions.

RAND is a nonprofit institution that helps improve policy and decisionmaking through research and analysis. RAND's publications do not necessarily reflect the opinions of its research clients and sponsors.