Protocol verification is an activity to assure the correctness of comm
unication protocols. Global state reachability analysis is one of the
most straightforward and easily automated protocol verification method
s. This paper proposes an incremental protocol verification method for
the Extended Communicating Finite State Machine (ECFSM) model. Increm
ental protocol verification allows protocols to be modified at the run
time of global state reachability analysis. Then, instead of re-explo
ring the modified protocols from scratch, global state reachability an
alysis is continued incrementally at the modification point. To enhanc
e the efficiency, the proposed method incorporates the dead and live v
ariables concept that is used in Chu and Liu's global state reduction
technique (Chu and Liu, 1989). Using the proposed incremental protocol
verification method, incremental protocol design environments are ach
ievable for ECFSM-based Formal Description Techniques (FDTs), e.g. ISO
's Estelle. Our application of the proposed method to Estelle is also
briefly introduced in this paper.