An integrated algorithm for probabilistic protocol verification and evaluation

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 computa...

Full description

Saved in:
Bibliographic Details
Main Authors: Dimitrijevic, D.D., Chen, M.-S.
Format: Conference Proceeding
Language:English
Subjects:
Computational complexity
Costs
Explosions
Hardware
Protocols
Reachability analysis
System recovery
Throughput
Time measurement
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.< >
DOI:10.1109/INFCOM.1989.101435