A top-down step-wise refinement methodology for protocol specification

Existing approaches to formal protocol specification and verification suffer from great difficulty in constructing correct specifications for practical problems. The objective of this paper is to advocate a top-down step-wise refinement approach in the construction of correct protocol specification, from the given requirement (a service specification). It is aimed at making formal specification a practical means to protocol design. The paper demonstrates the feasibility of the methodology by working on a non-trivial problem using a powerful specification formalism.