1.一种基于谓词依赖图的EFSM可执行测试序列生成方法，包括如下步骤：

(1)分析EFSM中各变迁涉及的变量类型及变量使用类型；

(2)对于EFSM中的任一赋值使用类型的变迁，确定与其存在数据依赖关系的变迁，使存在数据依赖关系的两个变迁构成谓词依赖对，且令谓词依赖对中赋值使用类型的变迁为头变迁，另一变迁为尾变迁；依此遍历EFSM中的所有赋值使用类型的变迁，并建立EFSM的谓词依赖图；

(3)分析谓词依赖对的三重属性：即头变迁涉及的变量类型和赋值运算符类型以及尾变迁涉及的谓词判断符类型；

(4)建立谓词依赖矩阵M，根据谓词依赖对的三重属性从谓词依赖矩阵M中提取谓词依赖对所对应的谓词依赖预测值；

(5)根据谓词依赖预测值，计算谓词依赖图中每个变迁的可执行预测值；

(6)从EFSM中任选一个状态作为初始状态，以该初始状态为根节点构建EFSM的可执行分析树，并对可执行分析树进行路径搜索：当从可执行分析树中搜索到一条变迁且初始状态到该变迁尾状态的路径满足用户的覆盖要求，即终止搜索，并输出该路径作为EFSM的可执行测试序列。

2.根据权利要求1所述的EFSM可执行测试序列生成方法，其特征在于：所述的变迁涉及的变量类型为常数、输入变量或上下文变量三类，变迁涉及的变量使用类型为赋值使用类型或谓词使用类型两类。

3.根据权利要求1所述的EFSM可执行测试序列生成方法，其特征在于：所述的谓词依赖图以EFSM中的变迁作为节点，任一组谓词依赖对的头变迁与尾变迁相连，未归于谓词依赖对的变迁不纳入谓词依赖图中。

4.根据权利要求1所述的EFSM可执行测试序列生成方法，其特征在于：所述的头变迁涉及的赋值运算符类型为+、-或nop三类；所述的尾变迁涉及的谓词判断符类型为≤&＜、≥&＞、＝或≠四类。

5.根据权利要求1所述的EFSM可执行测试序列生成方法，其特征在于：所述的谓词依赖矩阵M的表达式如下：其中：α、β和γ均为矩阵参数，谓词依赖矩阵M的第1至9行分别对应谓词依赖对头变迁的九种类型A1～A9，谓词依赖矩阵M的第1至4列分别对应谓词依赖对尾变迁的四种类型B1～B4；A1表示头变迁涉及的变量类型为上下文变量且赋值运算符类型为+，A2表示头变迁涉及的变量类型为常数且赋值运算符类型为+，A3表示头变迁涉及的变量类型为输入变量且赋值运算符类型为+，A4表示头变迁涉及的变量类型为上下文变量且赋值运算符类型为-，A5表示头变迁涉及的变量类型为常数且赋值运算符类型为-，A6表示头变迁涉及的变量类型为输入变量且赋值运算符类型为-，A7表示头变迁涉及的变量类型为上下文变量且赋值运算符类型为nop，A8表示头变迁涉及的变量类型为常数且赋值运算符类型为nop，A9表示头变迁涉及的变量类型为输入变量且赋值运算符类型为nop，B1表示尾变迁涉及的谓词判断符类型为＝，B2表示尾变迁涉及的谓词判断符类型为≤&＜，B3表示尾变迁涉及的谓词判断符类型为≥&＞，B4表示尾变迁涉及的谓词判断符类型为≠。

6.根据权利要求1所述的EFSM可执行测试序列生成方法，其特征在于：所述的步骤(5)中根据以下算式计算变迁的可执行预测值：其中：T表示变迁，fvalue(T)表示变迁T的可执行预测值，m为谓词依赖图中的节点总数，Cmax为谓词依赖矩阵M中的最大元素值，n为初始状态到变迁T头状态的路径相对于用户的覆盖要求中未覆盖的变迁条数，k为变迁T与n条未覆盖的变迁能够组成谓词依赖对的数量，PDi为变迁T与n条未覆盖的变迁能够组成的k组谓词依赖对中的第i组谓词依赖对的谓词依赖预测值，i为自然数且1≤i≤k，Level(T)为变迁T头状态在可执行分析树中的层数，μ为预测参数且为大于0的自然数。

7.根据权利要求1所述的EFSM可执行测试序列生成方法，其特征在于：所述的步骤(6)中根据以下方法对可执行分析树进行路径搜索：①将初始状态所连的所有变迁纳入变迁格局集合中，并从该集合中提取出一条可执行预测值最大的可执行变迁作为当前变迁；

②判断初始状态到当前变迁尾状态的路径是否满足用户的覆盖要求：若是，则终止搜索；若否，则将当前变迁尾状态所连的其他所有变迁纳入变迁格局集合中，执行步骤③；

③从变迁格局集合中提取出一条可执行预测值最大的可执行变迁更新作为当前变迁，并返回执行步骤②，直至初始状态到当前变迁尾状态的路径满足用户的覆盖要求，即终止搜索。