Incremental maximal progress protocol verification for ECFSM-based protocols

Protocol verification is an activity involving detection of logical errors in communication protocols. In this paper, we propose an integrated approach to protocol verification. We modify the Communicating Finite State Machine (CFSM)-based maximal progress state reduction technique so that it is Extended Communicating Finite State Machine (ECFSM)-based. Next, we propose an ECFSM-based incremental protocol verification technique based on the maximal progress principle. To further reduce the number of global states to be explored, the dead and live variables concept is incorporated. As a result, an incremental maximal progress protocol verification method is derived based on the integration approach. Our ECFSM-based method is, therefore, applicable to the ECFSM-based Formal Description Techniques (FDTs), e.g., the International Standard Organization's (ISO) Estelle or International Telegraph and Telephone Consultative Committee's (CCITT) Specification and Description Language (SDL). Based on the incremental maximal progress verification method, an Estelle-based Incremental Maximal progress Protocol Verification System (EIMPVS) is developed on SUN SPARC workstations. In this way, protocol designers can use our EIMPVS to verify Estelle-specified protocols.