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 verification method, which is called reverse protocol verification. 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, 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 and the protocol under designing does have some logical errors; alternatively, 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 reverse method, an incremental protocol specification system (IPSS) has been developed on SUN SPARC workstations. Usage and applications of IPSS are also presented in this paper.