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

C. M. Huang, J. M. Hsu

研究成果: Article

摘要

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.

原文English
頁(從 - 到)177-192
頁數16
期刊Computer Communications
23
發行號2
DOIs
出版狀態Published - 2000 一月 15

All Science Journal Classification (ASJC) codes

  • Computer Networks and Communications

指紋 深入研究「PPP (P<sup>3</sup>): An Estelle-based Probabilistic Partial Protocol verification system」主題。共同形成了獨特的指紋。

  • 引用此