Feasibility Analysis of the EFSM Transition Path Combining Slicing with Theorem Proving

It is an important problem to generate test data from EFSM model in model-based testing, but it is time-wasting to generate test data for the infeasible paths, so determining the feasibility of the paths before generating test data for them is necessary. The feasibility of EFSM transition paths is analyzed by combing slicing with theorem proving. It is divided into two phases. In the first phase, the transitions related to the predicate on each transition in the path are got by backward slicing. And in the second phase, the feasibility of the path is determined by theorem proving to prove whether the post-condition of the transitions related to the predicate implying the predicate or not. Experimental result shows that the feasibility of the paths can be decided effectively and the number of theorem proving is reduced greatly, the infeasibility of the path also can be checked quicker by the proposed method.