An integrated algorithm for probabilistic protocol verification and evaluation

Abstract
An integrated approach is presented to probabilistic verification and performance evaluation of a communication protocol. The approach, following 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/sup 4/) to O(n/sup 2/m) in generating n states and exploring m transitions. This procedure (1) is computationally very efficient; (2) 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) takes important reliability measures as its stopping criteria.

This publication has 2 references indexed in Scilit: