Verification of a reliable net protocol

Abstract

We specify and prove correctness of a real-world fault-tolerance algorithm. The algorithm, developed by Chang and Maxemchuk [CM84], guarantees delivery of broadcast messages over a broadcast medium (e.g., an ethernet) in the presence of faults that may cause messages to be lost or only partially delivered. Instead of describing the operation of the algorithm in pseudo-code, as the authors of the algorithm have done, we generate a precise mathematical specification which is amenable to reasonably simple proof techniques. The formal method that we use in this paper is based on modal (state dependent) functions called the modal primitive recursive (m.p.r.) functions. Our analysis clarifies the workings of the algorithm by discarding the complex program scaffolding that obscures the original exposition.