一种基于约束的系统故障注入方法

摘要

本发明公开了一种基于约束的系统故障注入方法。步骤为，按照原子条件取反、合取范式子句取反策略将约束划分到原子条件、合取范式子句层次，在这些层次上求取规约约束的一组否定形式，作为故障数据生成的基础；将取反后约束中的约束变量使用正常输入组合替代，然后逐步对约束变量进行松弛替换，通过约束求解操作找到松弛变量数量最少、最接近真实情况的极小变异故障数据；利用极小变异故障数据作为测试输入，对待测系统实施故障注入并得到故障注入结果。本发明通过采用新的故障注入技术，生成了更真实、充分性更高的故障数据，加强了故障注入的检错能力，同时接近正常状态的故障也有利于测试人员修复和排除缺陷。

权利要求

1.一种基于约束的系统故障注入方法，其特征在于，包括以下步骤：

(1)按照原子条件取反、合取范式子句取反策略将约束划分到原子条件、合取范式子句层次，在这些层次上求取规约约束的一组否定形式，作为故障数据生成的基础；

(2)首先将取反后约束中的约束变量使用正常输入组合替代，然后逐步对约束变量进行松弛替换，通过约束求解操作找到松弛变量数量最少、最接近真实情况的极小变异故障数据；

(3)利用极小变异故障数据作为测试输入，对待测系统实施故障注入并得到故障注入结果。

2.根据权利要求1所述基于约束的系统故障注入方法，其特征在于，在步骤(1)中，所述原子条件取反策略的步骤如下：首先判断输入的规约约束是否是原子约束，若为原子约束，则直接返回约束的否定；否则，逐个对输入的规约约束的顶层逻辑操作符的各个算子进行取反，用取反后结果替换原有算子，并将结果加入到故障约束集中。

3.根据权利要求1所述基于约束的系统故障注入方法，其特征在于，在步骤(1)中，所述合取范式子句取反策略的步骤如下：首先，将输入的规约约束按合取操作进行分解，分解成多个合取范式子句，构成范式子句集合；

然后，遍历上一步得到的范式子句集合，在约束的合取范式表达式中，使用范式子句的否定替换范式子句得到故障约束，并加入到故障约束集中。

4.根据权利要求1所述基于约束的系统故障注入方法，其特征在于，在步骤(2)中，首先将故障数据完全地设定为一个正常数据组合，然后撤销对正常数据中一个变量的取值指派，被撤销指派的变量将作为候选变异变量，对该变异变量进行约束求解检测，检测是否能够找到一个满足取反后约束的解，若能找到，则该变异变量的解和其它未变异部分的组合构成极小变异故障数据；若不能找到，则逐步对取反后约束中的其它变量进行松弛替换，直到获得一个解为止。

5.根据权利要求1所述基于约束的系统故障注入方法，其特征在于，在步骤(3)中，故障注入过程截获到特定的软件内部或外部接口，然后将步骤(2)得到的极小变异故障数据发送到相应的接口，实现故障注入；通过观察注入故障后待测系统是否出现异常，考查待测系统的容错能力。

说明书

一种基于约束的系统故障注入方法

技术领域

[0001] 本发明属于计算机系统开发技术领域，特别涉及了一种基于约束的系统故障注入方法。

背景技术

[0002] 故障注入是一种系统可靠性(Dependability)验证技术，通过在实验中向待验证系统刻意引入故障，检测观察故障引入之后的系统行为来检测系统的可靠性。在现有的故障注入方式一般为注入异常数据和注入异常代码。前者例如E.Jeong等人根据故障模型生成异常数据，并把异常数据通过消息拦截等方式注入到系统中；后者例如R.Natella等人通过在源码层或二进制层注入异常代码，间接产生故障状态，达到故障注入的目的。

[0003] 在故障数据注入方面，一些方法生成硬件或通信故障，如J.H.Barton等人提出的位翻转、字节修改等，以及S.Han等人提出的消息丢失、消息重复、消息头尾对调、消息延迟等。另一些方法生成软件故障，包括基于模式的故障生成方法、基于数据类型的故障生成方法、基于文法的故障生成方式等。基于模式的生成根据经验的故障模式生成故障，例如生成空指针或错误的函数返回代码，以检测目标系统的行为。基于数据类型的生成方式依据数据类型对数据进行分组，然后选择典型的异常值，例如类型的边界值，进行故障注入。基于文法的生成方式描述输入的文法结构，然后基于文法生成异常格式的数据进行注入。Johansson等人及Winter等人还研究了多种注入方式的组合，同时注入多种错误来增强故障注入发现错误的能力。上述方法一般可以生成格式、范围等明显异常的数据，但难以生成格式良好，却逻辑上不为合理的故障状态，应用范围存在较大限制。在现实中，很多隐蔽的错误都是由于结构上合理，但逻辑不合理的错误状态导致的，为揭示这些错误，必须采用具有逻辑异常数据生成能力的故障注入技术。

[0004] 基于约束的故障注入为逻辑异常数据的生成提供了契机。Godefroid等人的SAGE工具利用白盒符号执行来导出给定程序路径对应的路径约束，然后对路径约束中的谓词进行取反以生成新的测试输入。这种方法能够生成相对约束条件而言，逻辑上不合理的故障数据，但其在黑盒测试场景下，难以获知约束条件中哪些部分对应程序路径上的判定谓词，因此SAGE中的约束取反方法并不适用于黑盒测试场景。另一方面，SAGE方法通过约束求解获得全新的输入数据组合来进行测试，所生成的故障数据不能保证接近真实情况，故障注入的缺陷检测能力无法保证。

发明内容

[0005] 为了解决上述背景技术提出的技术问题，本发明旨在提供一种基于约束的系统故障注入方法，基于规约约束导出一组覆盖充分性好、真实性高的故障数据，从而有效地检测系统的可靠性缺陷。

[0006] 为了实现上述技术目的，本发明的技术方案为：

[0007] 一种基于约束的系统故障注入方法，包括以下步骤：

[0008] (1)按照原子条件取反、合取范式子句取反策略将约束划分到原子条件、合取范式子句层次，在这些层次上求取规约约束的一组否定形式，作为故障数据生成的基础；

[0009] (2)首先将取反后约束中的约束变量使用正常输入组合替代，然后逐步对约束变量进行松弛替换，通过约束求解操作找到松弛变量数量最少、最接近真实情况的极小变异故障数据；

[0010] (3)利用极小变异故障数据作为测试输入，对待测系统实施故障注入并得到故障注入结果。

[0011] 进一步地，在步骤(1)中，所述原子条件取反策略的步骤如下：

[0012] 首先判断输入的规约约束是否是原子约束，若为原子约束，则直接返回约束的否定；否则，逐个对输入的规约约束的顶层逻辑操作符的各个算子进行取反，用取反后结果替换原有算子，并将结果加入到故障约束集中。

[0013] 进一步地，在步骤(1)中，所述合取范式子句取反策略的步骤如下：

[0014] 首先，将输入的规约约束按合取操作进行分解，分解成多个合取范式子句，构成范式子句集合；

[0015] 然后，遍历上一步得到的范式子句集，在约束的合取范式表达式中，使用范式子句的否定替换范式子句得到故障约束，并加入到故障约束集中。

[0016] 进一步地，在步骤(2)中，首先将故障数据完全地设定为一个正常数据组合，然后撤销对正常数据中一个变量的取值指派，被撤销指派的变量将作为候选变异变量，对该变异变量进行约束求解检测，检测是否能够找到一个满足取反后约束的解，若能找到，则该变异变量的解和其它未变异部分的组合构成极小变异故障数据；若不能找到，则逐步对取反后约束中的其它变量进行松弛替换，直到获得一个解为止。

[0017] 进一步地，在步骤(3)中，故障注入过程截获到特定的软件内部或外部接口，然后将步骤(2)得到的故障数据发送到相应的接口，实现故障注入；通过观察注入故障后待测系统是否出现异常，考查待测系统的容错能力。

[0018] 采用上述技术方案带来的有益效果：

[0019] 本发明对约束进行不同粒度的划分和取反，进而导出不同覆盖程度的逻辑上不合理的故障数据，具有较高的故障注入测试覆盖率，从而可以较为充分地检测系统对逻辑故障的容错性。在测试数据的生成过程中，采用极小变异的方式生成测试数据，而不是直接对约束进行求解，以确保生成的故障数据尽可能地接近原始正常数据，接近正常数据的故障数据，更有可能在真实系统中发生，因此也越能够有效地检测系统的可靠性缺陷。接近真实情况的故障数据也能使故障注入引起的故障更容易被调试。

附图说明

[0020] 图1是本发明的流程图；

[0021] 图2是不同粒度的约束取反策略示意图；

[0022] 图3是极小变异故障数据生成示意图。

具体实施方式

[0023] 以下将结合附图，对本发明的技术方案进行详细说明。

[0024] 一种基于约束的系统故障注入方法，如图1所示，步骤如下。

[0025] (1)规约约束取反。按照原子条件取反、合取范式取反策略将约束划分到原子条件、合取范式子句层次，在这些层次上求取规约约束的一组否定形式，作为故障数据生成的基础。

[0026] (2)极小变异故障数据生成。首先将取反后约束中的约束变量使用正常输入组合替代，然后，逐步对约束变量进行松弛替换，通过约束求解操作找到松弛变量数量最少、最接近真实情况的故障数据。

[0027] (3)故障注入实施。利用上述步骤生成的测试数据作为测试输入对待测试系统实施故障注入并得到故障注入结果。

[0028] 步骤(1)中的约束划分是指在测试过程中根据测试覆盖体系的要求将约束划分到不同层次，在划分后的层次上对约束进行取反操作，得到整个规约约束的否定形式。具体的划分取反策略包括划分到原子条件进行取反，以及将约束划分到合取范式进行取反。其中原子条件是不可再进行划分的约束，合取范式的每个子式不可再进行合取分解的子式。不同层次的划分，对应不同的测试覆盖要求，其中原子覆盖和合取范式子式覆盖具有较高的测试覆盖率。

[0029] 步骤(2)中的极小变异故障数据生成，首先，将故障数据完全地设定为一个正常数据组合，正常数据可以通过对被测系统进行监控获得。然后，撤销对正常数据中一个变量的取值指派，被撤销指派的变量将作为候选变异变量。对变异变量，通过约束求解检测是否可找到一个满足取反后约束的解，若能找到，则该变异变量的解和其它未变异部分的组合即为构成异常的故障数据。若无法找到可满足解，则逐步对取反后约束中的其它变量进行松弛替换，直到获得一个解为止。此解即与正常执行数据最为接近的故障数据，具有较高的可能在真实系统中发生，用其来进行故障注入测试比用不太可能在真实系统中发生的异常数据更能够发现可靠性缺陷。

[0030] 步骤(3)中故障注入可通过消息拦截、API挂钩等技术实现。

[0031] 下文将对如何具体实施上述技术方案进行进一步说明。

[0032] 第一阶段(约束取反)

[0033] 对于给定的规约约束按不同粒度的策略取反，得到用于故障数据生成的故障约束集。每个取反后的约束是原始规约约束的一种否定形式，如果这些约束得到满足，那么原始规约约束一定取值为假，表明满足取反后约束的数据组合对应了逻辑上不合理的故障数据。因为取反后约束代表了故障数据，是故障数据的模型表达，也称这种约束为故障约束。对于给定规约约束，存在多种取反策略以得到其不同否定形式。现有黑盒故障注入测试主要是进行约束整体取反，即在约束前加上取反操作，得到约束的否定形式，这种方式无法保证取反后的约束覆盖各种可能存在的故障情况，故障注入覆盖率低。而本发明新提出了原子约束取反和合取范式子句取反两种能够实现更高测试覆盖的取反策略。图2是不同粒度的约束取反策略示意图。

[0034] 1)原子约束取反

[0035] 一个规约约束一般由多组不可分解的内部约束通过合取、析取或否定等逻辑操作符连接而成。这些不包含任何逻辑操作符、不可分解的约束称为原子约束。原子约束取反主要在原子约束层次对约束条件进行取反。简单地对原子约束取否定并不能保证取反后约束成立时，所对应的输入数据一定是逻辑上不合理的故障数据，另外，原子约束中所含的变量信息较少，也不能用于构造完成的故障输入。为此，本方法通过原子约束取反外再合取一个整体约束的否定保证取反后的约束可满足时，原始规约约束一定不可满足，且保证所生成故障数据的完整性。算法1给出了原子约束取反的递归处理算法。

[0036]

[0037] 算法首先判断输入约束是否是原子约束，若为原子约束，则直接返回约束的否定。否则，逐个对输入约束的顶层逻辑操作符的各个算子进行取反，用取反后结果替换原有算子，并将结果加入到作为结果的故障约束集中。其中，输入约束非原子约束的操作具体步骤为首先得到输入约束C的顶层操作对象集合；然后遍历集合中的操作对象，以这些对象对应的子约束为输入，递归地使用原子约束取反算法得到子约束对应的子故障约束集；遍历子故障约束集，使用子故障约束集中的约束替代输入约束C中对应的子约束得到新的约束，将得到的约束与输入约束C的否定进行合取，得到故障约束并加入故障约束集中。

[0038] 2)合取范式子句取反

[0039] 合取范式子句取反策略对原有规约约束的各个合取范式子句进行取反，以得到原约束的否定形式。设C1,C2,…,Cn是约束C的合取范式子句，则C＝C1∧C2∧…∧Cn，其中Ci(1≤i≤k)是原子约束或常量(例如P或 P)的析取结果。对约束C的一个合取范式子句取反即对约束C的合取范式的一个子句Ci用它的否定形式 Ci进行替换。算法2给出了合取范式子句取反算法。

[0040]

[0041] 第一步：将输入的规约约束按合取操作进行分解，分解成多个合取范式子句，构成范式子句集合。例如，若C＝(P∨Q)∧R，则分解后得到的合取范式子集为{(P∨Q),R}。由于此处获得合取范式的目的是确保对原约束进行有效划分，以用于生成故障输入，本方法不采用引入大量临时变量的Tseitin方法来进行合取范式变化，而是基于De Morgan律、吸收律和分配律进行合取范式变换。

[0042] 第二步：遍历范式子句进行取反。遍历上一步得到的范式子句集，在约束的合取范式表达式中，使用范式子句的否定替换范式子句得到故障约束，并加入到故障约束集中。例如，对C＝(P∨Q)∧R的取反结果为此处本方法以替换范式子句的方式得到
故障约束，而不是直接以范式子句的取反形式作为故障约束。后者虽然也能够导出故障数据，但其无法保证除范式子句外对输入的其它限制都尽量保持不变，因此生成出的故障数据可能与原始正常数据差异过大，故障真实性不佳，而本方法则能够保证故障数据的限制条件与原始正常数据尽量相近，只有小部分不同，上述特征的故障约束可为后续更真实故障数据的生成奠定基础。

[0043] 第二阶段(极小变异故障数据生成)

[0044] 极小变异故障生成在原有正常测试数据的基础上，引入最少的变化，以使得变异出的故障数据一方面能令故障约束(原规约约束的否定形式)得到满足，代表逻辑上不合理的取值；另一方面使故障数据尽可能接近原始正常数据，从而保证注入的故障状态接近真实情况中可能发生的异常。

[0045] 本发明采用约束变量逐步松弛的方法生成故障数据。算法开始先将故障约束中的每个约束变量的取值限定为正常测试数据取值。正常取值不能使故障约束得到满足，因此需要逐步松弛对约束变量的限制，直到松弛后故障约束可以获得可满足的解，这些解即极小变异故障。算法3给出了具体故障数据生成算法。图3是故障数据生成方法示意图。

[0046]

[0047] 算法首先假定初始松弛的约束变量集Vrelax为空，将每个约束变量限定到原始取值指派A上，使用约束求解器求解故障约束，检查是否有解。若有解，这该解即极小变异故障，获得解后算法即可返回。

[0048] 如果上一步无法求解出极小变异故障，则进一步进行变量松弛。在变量赋值指派A中选择一个新的变量添加到松弛变量集Vrelax中，递归地将故障约束和新的松弛变量集作为参数代入到本算法中，计算在新的松弛变量集的情况下是否能生成故障数据。若能生成非空的故障数据集F’，则将所得到的数据合并到最终的故障数据集F中，由此得到极小变异故障集。

[0049] 第三阶段(故障注入实施)

[0050] 本发明通过上述步骤生成高覆盖度、强真实性的故障数据，在获得故障数据后，利用已有消息拦截、API挂钩等技术实施故障注入。故障注入过程截获到特定的软件内部或外部接口，然后将本发明所生成的故障数据发送到相应的接口，即可实现故障的注入。通过观察注入故障后被测系统是否出现宕机等异常，可以考查被测系统的容错能力。

[0051] 为验证本发明的优越性，我们在GNU Coreutils-6.11数据集中的16个基准程序(见表1)上开展了实验。通过比较采用与不采用极小变异故障数据生成技术时所得故障数据与原始正常数据在输入层面的相似性，可以验证本发明所得的故障数据是否具有更佳的真实性。通过比较采用原子条件取反、合取范式取反两种新策略所得测试数据与采用传统的整体取反策略所得测试数据所能达到的语句和分支覆盖，可以验证本发明是否能够通过细粒度的取反策略实现更高的故障注入测试覆盖。

[0052] 表2展示了不同取反策略下，是否采用极小变异故障数据生成所得到的异常数据与原有正常数据相比在输入层面的相似度。其中，CON、CNF、WHOLE分别代表原子约束取反、合取范式子句取反、约束整体取反三种取反策略下的故障数据生成。用min下标表示带极小变异的故障数据生成。在原子约束取反方面，在14个实验对象上使用极小变异生成了更接近正常值的故障数据。在合取范式子句取反方面，使用极小变异方法在所有实验对象都能生成更接近正常值的故障数据。在约束整体取反方面，除了split程序外，使用极小变异方法生成的故障数据明显与正常数据有着更高的相似性。因此，对于90％以上的实验对象，使用极小变异的方法能生成更接近原始输入的故障数据，所得数据有更高的真实性。

[0053] 表3显示了不同策略下对各实验对象进行故障注入所达到的语句覆盖(SC)和分支覆盖(BC)。WHOLEcon、WHOLEcnf表示对约束整体取反，且生成与CON和CNF策略相一致规模的故障数据集。语句覆盖方面，15个实验对象上原子约束取反比合取范式子句达到更高的覆盖率，并且相较于整体约束取反，原子约束取反全都得到更好的覆盖。范式子句取反在15个实验对象上比约束整体取反得到更好的覆盖。分支覆盖方面，可得到与语句覆盖相似的结果。由此可见，通过应用本发明中的细粒度约束取反策略能够比已有的约束整体取反策略实现更高的故障注入测试覆盖。

[0054] 表1

[0055] 程序 描述 代码行base64 加密/解密数据和输出到标准输出中 3989
chcon 更改文件安全上下文 4343
chgrp 改变组的所有权 4278
comm 逐行比较两个排序文件 3997
cut 从文件中每行删除部分。 4195
dircolors ls颜色设置 4093
expand 将制表符转换为空格 3916
expr 表达式求值 9565
fold 将每个输入行包裹在指定的宽度中 3891
mknod 设置块或字符的特殊文件。 3840
paste 合并文件 3837
pathchk 检查文件名是否有效或可移植。 3857
printf 通过mailcap文件中的条目执行程序。 4251
split 文件分割 4428
sum 校验和计数文件中的块。 4068
tsort 进行拓扑排序 3856

[0056] 表2

[0057]程序 CONmin CON CNFmin CNF WHOLEmin WHOLE
base64 0.45 0.33 0.26 0.06 0.76 0.05
chcon 0.49 0.35 0.36 0.24 0.82 0.07
chgrp 0.61 0.39 0.40 0.29 0.77 0.05
comm 0.52 0.41 0.39 0.30 0.89 0.05
cut 0.52 0.48 0.25 0.22 0.74 0.07
dircolors 0.52 0.42 0.56 0.53 0.70 0.06
expand 0.42 0.42 0.34 0.06 0.85 0.05
expr 0.58 0.30 0.25 0.15 0.61 0.04
fold 0.32 0.32 0.29 0.25 0.86 0.10
mknod 0.48 0.41 0.42 0.41 0.66 0.06
paste 0.50 0.52 0.29 0.24 0.80 0.06
pathchk 0.40 0.30 0.13 0.00 0.78 0.04
printf 0.62 0.42 0.44 0.20 0.62 0.04
split 0.26 0.26 0.24 0.23 0.18 0.23
sum 0.45 0.35 0.38 0.09 0.69 0.06
tsort 0.72 0.63 0.31 0.00 0.80 0.04
Average 0.49 0.39 0.33 0.20 0.72 0.07

[0058] 表3

[0059]

[0060]

[0061] 实施例仅为说明本发明的技术思想，不能以此限定本发明的保护范围，凡是按照本发明提出的技术思想，在技术方案基础上所做的任何改动，均落入本发明保护范围之内。