Efforts at protocol verification have involved a number of formal models such as Petri nets, UCLA Graphs, state diagrams, and assertions. The powerful general theory developed for these abstract models has been brought to bear on various aspects of protocol operation and has succeeded in verifying some facets of protocol reliability. This paper surveys recent work in verifying the correct operation of communication protocols for computer networks. Unfortunately, both the complexity of more powerful protocols, and more hostile transmission media are beyond the capabilities of current formal models. Assertion techniques have been most successful to date in verifying data transfer aspects of protocols. Analysis of control functions is less advanced, and consequences of protocol failures have been almost totally ignored. Despite the limited success of some formal models, verification of many "real world" protocols must still rely on less rigorous techniques of broader applicability.
This report is part of the RAND Corporation Paper series. The paper was a product of the RAND Corporation from 1948 to 2003 that captured speeches, memorials, and derivative research, usually prepared on authors' own time and meant to be the scholarly or scientific contribution of individual authors to their professional fields. Papers were less formal than reports and did not require rigorous peer review.
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.
The RAND Corporation 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.