A multi-event-one-transition plus incremental processing protocol verification method

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's CFSM-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.