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

C. M. Huang, J. M. Hsu

Research output: Contribution to journalArticlepeer-review


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 (P3), is developed on SUN SPARC workstations. This way, protocol designers can use P3 to design and partially verify the Estelle-based protocol specifications.

Original languageEnglish
Pages (from-to)177-192
Number of pages16
JournalComputer Communications
Issue number2
Publication statusPublished - 2000 Jan 15

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications


Dive into the research topics of 'PPP (P<sup>3</sup>): An Estelle-based Probabilistic Partial Protocol verification system'. Together they form a unique fingerprint.

Cite this