Chung-Ming Huang, Huei-Yang Lai and Duen-Tay Huang
Institute of Information Engineering
National Cheng Kung University
Tainan, Taiwan 701, R.O.C.
Formal Description Techniques (FDTs), e.g. ISO's Estelle and CCITT's SDL, are becoming the standard mechanisms for specifying communication protocols. New protocol verification techniques, e.g., global state reduction techniques for FDT-based global state reachability analysis, are therefore required to verify FDT-specified protocols. Most of the currently existing global state reduction techniques are based on the Communicating Finite State Machine (CFSM) model. Therefore, these reduction techniques cannot be directly applied to ISO's Estelle or CCITT's SDL, which are Extended CFSM (ECFSM)-based Formal Description Techniques (FDTs), protocol verification systems. By modifying Itoh and Ichikawa'sCFSM-based reduction technique to be ECFSM-based, by modifying Huang et al.'s CFSM-based incremental verification technique to be ECFSM-based, and by incorporating Chu and Liu's ECFSM-based reduction technique, i.e., dead and live variable analysis, this paper proposes a Multi-event-one-transition Plus Incremental processing (MPI) protocol verification technique for verification of ECFSM-based n-entity protocols. In this way, the MPI verification technique can be directly applied to Estelle or SDL protocol verification systems.
Keywords: computer networks, communication protocols, protocol engineering, protocol verification
Received October 18, 1993; revised October 21, 1995.
Communicated by Jin-Fu Chang.
*This research was supported by the National Sciennce Council of the Republic of China under the grant NSC 81-0408-E-006-568.