INTEGRATED FDT-BASED PROTOCOL VERIFICATION SYSTEM

A communication protocol is a set of rules that govern interactions an d co-ordination among communicating entities in distributed systems an d computer networks. Therefore, deriving error-free protocols is cruci al to ensure reliable distributed systems and computer networks. A pro tocol verification software tool to design error-free protocols is pre sented. The Extended Communicating Finite State Machine (ECFSM) model, which belongs to the state transition model, is widely used to formal ly specify protocols with context variables and predicates. Global sta te reachability analysis is one of the most straightforward ways to ve rify communication protocols specified in the state transition model. By modifying a CFSM-based reduction technique to be ECFSM-based, then integrating with an ECFSM-based reduction technique, a new protocol ve rification technique for ECFSM-based n-entity protocols is proposed. T he integrated ECFSM-based verification technique can be directly appli ed to ISO's Estelle, which is an ECFSM-based Formal Description Techni que (FDT). With this technique, an Integrated FDT-based Protocol Verif ication System (IFPVS) is developed, which consists of an Estelle tran slator, a global state analyser, and a graphic user interface.