Backward protocol verification method and its applications

Chung Ming Huang, Duen Tay Huan

研究成果: Article同行評審


Protocol verification is an activity for ensuring the logical correctness of communication protocols. As computer networks become more popular and more complex, how to derive error-free protocols becomes an essential issue for providing reliable networking services. In this paper, we propose a new verification method, which is called backward protocol verification. A protocol is explored backwardly starting from a certain candidate erroneous global state. If none of the candidate erroneous global states belongs to the attainable global state, then the protocol is error-free. By analyzing the property of deadlock error, unspecified reception error, and channel overflow error, some candidate erroneous global states are generated accordingly. Then, each candidate global state is checked whether there is a path, i.e., a global state sequence, which can connect to the original initial global state. If there is a path, then the candidate global state is really an erroneous global state. Otherwise, if there is no candidate global state or none of the candidate global states has a path, then the protocol is error-free. Based on the backward method, a Backward Protocol Verification System (BPVS) is developed on SUN SPARC workstations.

All Science Journal Classification (ASJC) codes

  • 電氣與電子工程


深入研究「Backward protocol verification method and its applications」主題。共同形成了獨特的指紋。