Backward protocol verification method

Using the formal Communication Finite State Machine (CFSM) model, a communication protocol consists of several communicating entities which can be represented in some CFSMs. Global state reachability analysis is one of the most straightforward ways to automatically detect logical errors in a communication protocol specified in the CFSM model. Global state reachability analysis generates all of the reachable global states and checks the correctness one by one. Even though communication protocols are error free, global state reachability analysis still needs to be executed completely. In this paper, we propose a new verification method, which is called the backward protocol verification method, to detect logical errors. By analyzing the properties of deadlock error, unspecified reception error, and channel overflow error, some candidate erroneous global states are generated. Then, each candidate global state is checked whether there is a path, i.e., a global state sequence, connects to the original initial global state. If there is a path, then the candidate global state is really an erroneous global state and the communication protocol does have some logical errors. Otherwise, if there is no candidate global state or none of the candidate global state has a path, then the communication protocol is error free.