University of Texas at Austin Department of Computer Sciences
Networking Research Laboratory
Department of Computer Sciences
The University of Texas at Austin

Director: Simon S. Lam (more publications)

A Stepwise Refinement Heuristic for Protocol Construction

A. Udaya Shankar and Simon S. Lam

A stepwise refinement heuristic to construct distributed systems is presented. The heuristic is based upon a conditional refinement relation between system specifications, and a ``Marking.'' It is applied to construct four sliding window protocols that provide reliable data transfer over unreliable communication channels. The protocols use modulo-N sequence numbers. The first protocol is for channels that can only lose messages in transit. By refining this protocol, we obtain three protocols for channels that can lose, reorder and duplicate messages in transit. The protocols herein are less restrictive and easier to implement than sliding window protocols previously studied in the protocol verification literature.

General Terms:
Design, languages, verification
Additional Keywords and Phrases:
Assertional reasoning, conditional refinement, cyclic sequence numbers, interfaces, message lifetimes, sliding window protocols, stepwise refinement
* A. Udaya Shankar is on the faculty of the Department of Computer Science, University of Maryland, College Park