EHPVS: A PROTOCOL VERIFICATION SYSTEM FOR VERIFYING PROTOCOLS SPECIFIED IN ESTELLE

摘要

Protocol verification is an activity to detect logical errors in communication protocols. In this paper, we propose a hybrid technique for verifying protocols specified in the Extended Communicating Finite State Machine (ECFSM) model. The hybrid technique is achieved as follows: (1) modify the CFSM-based maximal progress state exploration technique to be ECFSM-based; (2) incorporate the dead and live variables concept. Our hybrid protocol verification technique is therefore applicable to ECFSM-based Formal Description Techniques (FDTs), e.g. ISO's Estelle or CCITT's SDL. Based on the hybrid verification technique, an Estelle-based Hybrid Protocol Verification System (EHPVS) has been developed on SUN SPARC workstations. In this way, protocol designers can use our EHPVS to verify Estelle-specified protocols.