Towards the Unification of the Functional and Performance Analysis of Protocols or, Is the Alternating-Bit Protocol Really Correct?

Yemini, Yechiam; Kurose, James F.

In the past 15 years the alternating-bit protocol has been perhaps the most widely verified protocol, the benchmark of protocol verification techniques; is it really correct? We claim that the answer is negative. The problem is that existing concepts of correctness do not capture an important sense in which a protocol may be incorrect. Specifically, although protocol goals (e.g., delivering messages) may be attained eventually, the time periods to achieve these goals may increase indefinitely. A notion of correctness which allows one to consider both the probability of reaching a goal as well as the time or computational effort required to achieve the goal is required. We present a novel approach to protocol correctness which unifies functional and performance considerations using a recently proposed probabilistic semantics for programs.



More About This Work

Academic Units
Computer Science
Department of Computer Science, Columbia University
Columbia University Computer Science Technical Reports, CUCS-026-82
Published Here
October 25, 2011


This work was supported in part by National Science Foundation Grant NSF MCS-8110319, the Defense Advanced Research Projects Agency and the IBM Corp.