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