Towards the Unification of the Functional and Performance Analysis of Protocols or, Is the Alternating-Bit Protocol Really Correct?
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.
- cucs-026-82.pdf application/pdf 311 KB Download File
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.