Correctness of At-Most-Once Message Delivery Protocols

Butler W. Lampson, Nancy A. Lynch, and Jorgen Sorgaard-Andersen

Citation: B. Lampson, N. Lynch, and J. Sorgaard-Andersen . Correctness of at-most-once message delivery protocols. Proc. 6th International Conference on Formal Description Techniques, Boston, 1993, pp 387-402.

Links: Abstract, Postscript, Acrobat. Slides for a less formal account of this topic are here. Here is an HTML version created by OCR for the benefit of search engines; it is not meant for human consumption.

Email: blampson@microsoft.com. This paper is at http://research.microsoft.com.

Abstract:

This paper addresses the issues of formal description and verification for communication protocols. Specifically, we present the results of a project concerned with proving correctness of two different solutions to the at-most-once message delivery problem. The two implementations are the well known five-packet handshake protocol and a timing-based protocol developed for networks with bounded message delays.

We use an operational automaton-based approach to formal specification of the problem statement and the implementations, plus intermediate levels of abstractions in a stepwise development from specification to implementations. We use simulation techniques for proving correctness.

In the project we deal with safety, timing, and liveness properties. In this paper, however, we concentrate on safety and timing properties.