Academic Commons


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.

Academic Commons provides global access to research and scholarship produced at Columbia University, Barnard College, Teachers College, Union Theological Seminary and Jewish Theological Seminary. Academic Commons is managed by the Columbia University Libraries.