Correctness of At-Most-Once Message Delivery Protocols
Butler Lampson, Nancy Ann Lynch, Jørgen F. Søgaard-Andersen · 1993
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. Keyword Codes: C.2.2; D.2.4; F.1.1 Keywords: Computer Systems Organization, Network Protocols; Software, Program Verification; Theory of Computation, Models of Computation 1. INTRODUCTION