Integrated FDT-based protocol verification system

A communication protocol is a set of rules that govern interactions and co-ordination among communicating entities in distributed systems and computer networks. Therefore, deriving error-free protocols is crucial to ensure reliable distributed systems and computer networks. A protocol verification software tool to design error-free protocols is presented. The extended communicating finite state machine (ECFSM) model, which belongs to the state transition model, is widely used to formally specify protocols with context variables and predicates. Global state reachability analysis is one of the most straightforward ways to verify 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 verification technique for ECFSM-based n-entity protocols is proposed. The integrated ECFSM-based verification technique can be directly applied to ISO´s Estelle, which is an ECFSM-based formal description technique (FDT). With this technique, an integrated FDT-based protocol verification system (IFPVS) is developed, which consists of an Estelle translator, a global state analyser and a graphical user interface