PPP (P³): An Estelle-based Probabilistic Partial Protocol verification system

Protocol verification is a process for checking the correctness of communication protocols. However, verifying practical and complicated protocols always encounters the state explosion problem using global state reachability analysis. In this paper, we propose a probabilistic partial protocol verification scheme to verify communication protocols that are specified in the extended state transition model, i.e. the Extended Communicating Finite State Machine (ECFSM) model. Based on our probabilistic verification scheme, the occurrence probability of each global state is derived using the occurrence rates of communicating entities' transitions and the occurrence probabilities of channel entities' transitions. Then, only those global states whose occurrence probabilities are greater than a given threshold need to be explored. As a result, probabilistic partial protocol verification can be achieved. In order to calculate more reasonable communicating transitions' occurrence rates and channel transitions' occurrence probabilities, we analyze protocol operations to derive transitions' probabilities relationships. Based on these relations, a reasonable value can be assigned to each transition's probability, which can be used to delimit partial probabilistic protocol verification. Using our probabilistic partial protocol verification scheme and derivation of transitions probabilities relationships, an Estelle-based Probabilistic Partial Protocol verification system, which is called PPP (P³), is developed on SUN SPARC workstations. This way, protocol designers can use P³ to design and partially verify the Estelle-based protocol specifications.