Analysis about transitivity of dependence relation in EFSM

摘要

Extended Finite State Machine (EFSM) is an important formal description technique, widely used in network communications protocol software, embedded systems, object-oriented software modeling. Using EFSM to describe the control flow and the data flow of the protocol can give the support for analysis, verification, and implementation on the protocol. As the network size and complexity increasing, EFSM's states and transitions grow rapidly, the protocol model becomes difficult to understand and test. Program slicing is an important Reduction technology, Apply this technology into the EFSM model, it can reduce the number of state and transition according to points of interest, and then reduce the set of fault diagnosis. So it is important to analysis and test on protocol. Because of the special dependence relation based on transition of EFSM model, the traditional dependence graph construction algorithm and tag-based slicing algorithm do not effective.