REVERSE PROTOCOL VERIFICATION - CONCEPT, ALGORITHM AND APPLICATION

To verify the logical correctness of communication protocols, protocol verification should be invoked in the design phase. In this paper, we propose a new communicating finite state machine (CFSM)-based verific ation method, which is called reverse protocol verification. By analyz ing the properties of deadlock error, unspecified reception error and channel overflow error, some candidate erroneous global states are gen erated. Then, each candidate global state is checked whether there is a path, i.e. a global state sequence, which can connect to the origina l initial global state. If there is a path, then the candidate global state is really an erroneous global state and the protocol under desig ning does have some logical errors; alternatively, if there is no cand idate global state or none of the candidate global states has a path, then the protocol is error free. Based on the reverse method, an incre mental protocol specification system (IPSS) has been developed on SUN SPARC workstations. Usage and applications of IPSS are also presented in this paper.