Director: Simon S. Lam (more publications)
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.