A procedure for probabilistic protocol verification

A new dynamic state exploration algorithm which is applied to probabilistic protocol verification and performance evaluation for synchronous as well as asynchronous models of a protocol is introduced. Properties of the technique are analyzed and proposed to further enhance the verification and evaluation procedure. The procedure based on this technique evaluates the importance of states in the dynamic course of a global reachability graph generation, explores only the most probable subset of states based on their dynamically computed importance, and quantifies and bounds important reliability and performance measures such as mean time to failure and turnaround time. Properties of the algorithm are demonstrated via the call establishment phase of the X.75 protocol.