Formal Methods in Communication Protocol Design

TLDR

Protocol design has evolved from informal, ad‑hoc approaches to rigorous formal techniques that define both the services a layer offers and the internal operations of its components, with verification ensuring that the implementation satisfies the specification. The paper surveys formal methods applied to protocol specification, verification, and implementation. The survey discusses state‑transition models, program verification, symbolic execution, and design rules as formal methods for protocol specification, verification, and implementation.

Abstract

While early protocol design efforts had to rely largely on seat-of-the-pants methods, a variety of more rigorous techniques have been developed recently. This paper surveys the formal methods being applied to the problems of protocol specification, verification, and implementation. In the specification area, both the service that a protocol layer provides to its users and the internal operations of the entities that compose the layer must be defined. Verification then consists of a demonstration that the layer will meet its service specification and that each of the components is correctly implemented. Formal methods for accomplishing these tasks are discussed, including state transition models, program verification, symbolic execution, and design rules.