扩展有限状态机EFSM的后向切片

切片是一种重要的约减技术，基于代码的程序切片已经得到广泛的研究和大量的应用，但基于规格和模型的切片研究不多．EFSM是一种重要的规格模型，将切片技术引入EFSM对于分析和测试基于EFSM的软件模型具有重要的作用．由于一个实际的EFSM相当复杂，导致对EFSM模型的分析和修改非常困难．EFSM的切片对于测试和分析EFSM模型具有重要意义．由于EFSM依赖关系的特殊性，依赖图的可达性问题对于EFSM依赖图中并不是一个简单的图可达性问题．而且现有的基于标志已访问节点的遍历算法不适于解决该问题．对EFSM的依赖关系的传递性进行了详细的讨论和分析，定义了一个递归的依赖传递函数来描述变迁的影响如何通过依赖关系传递，而计算后向切片则可以通过逆依赖传递函数来描述，最后给出一个基于变迁的EFSM后向切片算法