About cookies on this site Our websites require some cookies to function properly (required). In addition, other cookies may be used with your consent to analyze site usage, improve the user experience and for advertising. For more information, please review your options. By visiting our website, you agree to our processing of information as described in IBM’sprivacy statement. To provide a smooth navigation, your cookie preferences will be shared across the IBM web domains listed here.
Publication
IEEE INFOCOM 1989
Conference paper
An integrated algorithm for probabilistic protocol verification and evaluation
Abstract
This paper presents an integrated approach to probabilistic verification and performance evaluation of a communication protocol. The approach, following the Best-First rules, generates, verifies, and evaluates states and transitions in a global reachability graph. A new recursion is found to reduce the computational complexity of the procedure from O(n 4) to O(n 2m) in generating n states and exploring m transitions. This procedure is unique in that (1) it is computationally very efficient and (2) it provides interesting performance and reliability measures such as Mean Time To Unknown, which is the average operation time before any unchecked scenario occurs, and protocol throughput, and (3) it takes important reliability measures as its stopping criteria. © 1989 IEEE.