Backward protocol verification method and its applications

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.