Property verification of communication protocols based on probabilistic reachability analysis

In this paper we show how symbolic probabilistic analysis techniques for finite state systems can be successfully used to perform quantitative verification of properties and performance evaluation of communication protocols and, more in general, of entire protocol stacks and complete communication networks. In particular, we first outline our approach to the problem of verifying communication protocols, and then we present an application example of the proposed methodology to the simple Alternating Bit Protocol