© 1996 by British Computer Society
Reverse Protocol Verification: Concept, Algorithm and Application
1 Institute of Information Engineering, National Cheng Kung University, Tainan, Taiwan 70101, ROC, 2 Department of Applied Mathematics, National Sun Yat-Sen University, Kaohsiung, Taiwan 80424, ROC
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.
Received January 5, 1995. revised June 22, 1996.
* Institute of Information Engineering, National Cheng Kung University, Tainan, Taiwan 70101, ROC
Department of Applied Mathematics, National Sun Yat-Sen University, Kaohsiung, Taiwan 80424, ROC