Backward protocol verification method and its applications

Chung Ming Huang, Duen Tay Huan

Research output: Contribution to journalArticlepeer-review


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.

Original languageEnglish
Pages (from-to)153-168
Number of pages16
JournalJournal of the Chinese Institute of Electrical Engineering, Transactions of the Chinese Institute of Engineers, Series E/Chung KuoTien Chi Kung Chieng Hsueh K'an
Issue number3
Publication statusPublished - 1995 Aug 1

All Science Journal Classification (ASJC) codes

  • Electrical and Electronic Engineering


Dive into the research topics of 'Backward protocol verification method and its applications'. Together they form a unique fingerprint.

Cite this