Butler Lampson, Nancy Lynch and Joergen Soegaard-Andersen. Correctness of At-Most-Once Message Delivery Protocols, In R. L. Tenney, et al, editors, Formal Description Techniques, VI (Proceedings of the IFIP TC6/WG6.1 Sixth International Conference on Formal Description Techniques - FORTE '93 - Boston, MA, October 1993), IFIP Transactions C, pages 385-400, North Holland, 1994. .ps

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 abstraction in a step-wise 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.