A reduced incremental ECFSM-based protocol verification

The extended communication finite state machine (ECFSM) model, which belongs to the state transition model, has been used to formally specify protocols with context variables and predicates. Global state reachability analysis is one of the most straight-forward ways to verify communication protocols specified in the state transition model. Many CFSM-based global state reduction techniques have been proposed to reduce the complexity of global state reachability analysis. However, these reduction techniques cannot be directly applied to ISO´s Estelle and CCITT´s SDL, which are ECFSM-based formal description techniques (FDTs)-based protocol verification systems. Based on Itoh and Ichikawa´s (1983) CFSM-based, Chu and Liu´s (1989) ECFSM-based reduction techniques, and Huang et al.´s (1990) CFSM-based incremental verification technique, this paper proposes a protocol verification technique for ECFSM-based n-entity protocols. In this way, the integrated reduced incremental verification technique can be directly applied to Estelle or SDL -based protocol verification systems