摘要：为了达到运用切片技术对构件模型进行状态空间压缩的目的，在构件之间接口的交互关系的基础上，提出了用测试驱动节点和扩展的构件节点建立构件系统的功能依赖图的具体方法和步骤，并通过基于模型检验的接口变异测试方法对三角形问题的JavaBean构件在切片前后的模型分别进行了测试。实验结果表明，该方法能够有效地压缩系统的状态空间，提高测试效率，同时也保证了对构件接口测试的全面性和正确性。
关键词： 模型检验；接口变异；切片技术；功能依赖图
Abstract：Motivated by compressing the model of component through slicing technique， this paper employs the interactive relationship of the components. Then it proposes a method of constructing a function dependence graph for component system， which is made of a test driver node and some extended component nodes. Finally， by an example， it demonstrates that this method could not only decrease the size of the state space and increase the efficiency for testing generation， but also guarantee the comprehension and the validity of the interface testing for JavaBean components while applying the method of interface mutation testing based on model checking.
Key words： model checking； interface mutation； slicing technique； function dependence graph
尽管模型检验技术在自动化方面具有许多优点，但它是采用穷尽搜索系统空间的方法对所给定的性质进行验证，因此，对并发系统而言，其状态数往往随并发分量的增加呈指数增长，这样就产生了“状态空间爆炸”（state-explosion）问题[1]。对于基于模型检验的变异测试来说，当对非等价变异体采用“搜索所有的反例路径”的策略进行验证，以及对等价变异体进行验证时，都必须通过搜索整个系统的状态空间才能够进行判定，所以这样就影响了模型检验的验证效率。
因此，为了压缩系统状态空间的数量，本文将通过建立构件系统的功能依赖图，然后运用切片技术[4]对其进行切片。最后，本文将以Java PathFinder作为模型检验工具，采用基于模型检验技术的接口变异测试方法[5]对JavaBean构件进行接口变异测试，并对所切片效果进行验证。图1给出了该方法的测试用例生成框架。
1 构件系统的功能依赖图
S.Horwitz等人通过引入系统依赖图（System Dependence Graph，SDG）的概念表示了具有多个过程的程序依赖图[6]，但是使用该方法就必须知道每一个过程内部的具体细节信息，因此这种方法并不适用于在源码未知情况下的构件化软件切片；虽然文献[7]提出了一种能够对由构件所组成的系统进行切片的方法，但是这种方法却只考虑了构件之间接口的交互关系而忽略了构件在系统中的状态。因此，本文以文献[8]所提出的构件之间接口的交互关系为基础，在细化了构件之间的接口交互图后，使其能够在清晰描述源码未知情况下被测试构件的状态和接口函数之间的关系的同时，也能够使切片技术适用于对被测试构件系统的接口调用关系模型的状态空间的压缩。
1.1 功能依赖图的组成
本文以该被测试构件的接口规约说明为依据，通过测试驱动程序对被测试构件，或者是将该被测试构件和与之相关的构件关联后进行建模，从而建立被测试构件的接口调用关系模型。通过这个构件系统的接口调用关系模型，被测试构件所具备的相关功能会在利用模型检验技术进行验证的过程中表现出来。因此，将细化后的构件之间的接口交互关系称之为构件系统的功能依赖图（Function Dependence Graph，FDG），并且该图是由测试驱动节点（Test Driver Node）和构件节点（Component Node）两种类型的节点所组成。
测试驱动节点是由被测试构件的测试驱动程序所虚拟出来的一个节点，它是整个构件系统的主体框架。从切片技术的观点来分析，该节点实际上就是它所代表的测试驱动程序的过程依赖图[3]（Process Dependence Graph）。
构件节点实际上在代表被测试构件的同时，也可以代表与被测试构件相关联的构件。为了能够应用切片技术对其进行切片，需要通过添加一些辅助接点对构件节点及辅助边对其进行细化。这里通过定义一个五元组C = 来描述一个构件节点，具体如图2所示。 1） 构造函数辅助节点（Construction Assistant Node）的集合Con
对于JavaBean构件来说，为了体现面向对象的特征，在构件节点中应该添加与之相关的所有构造函数的构造函数辅助节点（Conk表示构件中第k个构造函数）。辅助节点实际上就是该构件的入口节点。
2） 状态辅助节点（State Assistant Node）的集合S
由于在代码未知情况下的构件接口测试是一种黑盒测试，因此，还必须在构件节点中添加表示构件状态的状态辅助节点（Si表示构件中第i个状态）。
3） 接口函数辅助节点（Interface Function Assistant Node）的集合I
在构件节点中添加表示该构件所包含的所有接口函数的接口函数辅助节点（Im表示构件中第m个接口函数）。
4） 输入参数辅助节点（Input Parameter Assistant Node）的集合p
对于每一个包含输入参数的接口函数应该在其所对应的接口函数辅助节点中添加表示该接口函数中所有参数的输入参数辅助节点（pn表示该接口函数中的第n个参数）。
5） 辅助节点之间辅助边（Assistant Edge）的集合E
为了能够体现出上述辅助节点之间的内在关系并使切片技术能够适用于构件节点，还必须根据构件的规约说明在辅助接点之间添加相应的边。首先，由于通过构造函数在实例化一个构件的时候，与该构件相关的状态和接口调用函数也会被创建，因此，就必须在构造函数辅助节点和状态辅助节点以及构造函数辅助节点和接口函数辅助节点之间添加一条控制依赖边；其次，根据构件的接口规约说明，应该在具有控制依赖关系的接口函数之间添加能够代表它们之间控制依赖关系的控制依赖边；最后，由于构件相关的状态信息是通过与之相关的构件接口函数进行改变的，所以需要在接口函数辅助节点和状态辅助节点之间添加一条控制依赖边，同时，构件的状态信息也需要通过接口函数向外界进行表现，因此，还应该在状态辅助节点和与之相关接口函数辅助节点之间添加一条数据依赖边。综上所述，构件节点之间辅助边的集合E是控制依赖边Ec和数据依赖边Ed的并集，即：E = Ec U Ed。
在明确了构件系统的功能依赖图的组成后，就应该根据测试驱动程序将测试驱动节点和构件节点进行关联，从而建立整个构件系统的功能依赖图，它主要包括建立测试驱动程序的过程依赖图和确立该过程依赖图与构件节点之间关联关系两个主要步骤。
文献[9]给出了建立测试驱动程序过程依赖图的具体方法和步骤，故本文在此不作熬述。
本文的研究重点在于对构件的接口进行测试，因此，对被测试构件系统的功能依赖图的建立主要就体现在确立测试驱动程序的过程依赖图和构件节点之间的关系之上，这些关系主要包括了如下四个方面：
1） 测试驱动程序对构件的实例化
在测试驱动程序中需要通过构造函数对JavaBean构件进行实例化。这样，就必须添加一条描述测试驱动程序对构件进行实例化的控制依赖边。
2） 测试驱动程序对构件中接口函数的调用
对构件中接口函数的每一次调用，需要添加一条描述测试驱动程序对接口函数进行调用的接口函数调用边。
3） 测试驱动程序对构件中接口函数的参数输入
对于拥有输入参数的接口函数来说，测试驱动程序在对其进行调用时，对于每一个输入参数都需要添加一条描述测试驱动程序在对其进行调用时的参数输入边。
4） 构件中接口函数对测试驱动程序的响应
对接口函数的调用实际上相当于对构件中相关功能进行了一次使用，因此，构件就必须向外界产生这个调用的一个响应，这样，就必须添加一条描述构件中接口函数响应的边。
本文以三角形问题的JavaBean构件为例进行研究，表1给出了三角形问题构件中的接口函数及接口函数所对应的状态。
建立构件系统的功能依赖图后，就可以运用切片技术对其进行切片。在基于模型检验技术的变异测试方法的测试用例的生成过程中，是通过引入断言违背机制将原有模型和变异模型结合并对构件的状态进行判定从而诱发错误生成并得到反例路径。因此，为了能够找到导致这个断言违背所产生错误的原因，就必须找到在这个断言违背之前，系统模型中哪些语句或者是哪个谓词表达式影响了所关注的这个断言违背，并且它们是如何传播到这个地方。这样在对功能依赖图进行切片时，就可以采用文献[6]中所提出的后向切片准则和两步图的可达性算法对构件系统的功能依赖图进行切片。
2 实验结果和分析
2.1 实验对象说明及实验结果
本节以三角形问题构件中反应三角形类型的状态“tType”作为兴趣点，对其构件系统的功能依赖图进行切片试验。图4所得到的即为切片后的三角形问题构件系统的功能依赖图。
在利用基于模型检验的接口变异测试方法对构件系统进行验证并生成测试用例时，为了能够体现出构件系统模型中存在的“状态空间爆炸”问题以及通过切片技术对系统的状态空间进行压缩后的效果，首先选择三角形问题构件的接口函数TriType（int a， int b， int c）的等价变异体TriType（int c， int b， int a）作为研究对象，并将三边的输入域划分为5组进行对比分析。 表2给出了在上述实验条件下，JPF对切片前后的构件系统在模型验证后所得到的状态数，它是由JPF统计信息中“state”里面的“new”与“visited”相加所得到的。
对表2进行分析可知：
首先，除去最后一行对压缩率的分析外，表格中的每一行都反应出随着三角形三边输入域的增加，整个模型检验过程所耗费的时间以及在验证过程中所产生的状态数都在以指数形式增加，这就体现了在本章最开始所提到的“状态空间爆炸”问题。
其次，表格中的每一列说明了在对构件接口调用关系模型运用切片技术后，模型检验工具在验证过程中所耗费的时间有了一定的减少，而且在整个验证过程中系统模型所产生的状态空间的数量也得到了压缩，模型检验的验证效率得到了提高。
再次，由于上述五组实验只改变了三角形问题构件的输入域，对于构件系统模型本身并没有进行改变，因此，在使用相同的切片准则并运用切片技术对构件系统的功能依赖图进行切片后，所得到的系统模型的状态空间压缩率在效果上基本是相同的。
最后。上述五组实验的验证结果都没有检验出任何反例路径，因此，切片技术的运用并不会影响“基于模型检验技术的接口变异测试方法”对等价变异体的正确判定。
2.2 统计分析
在上一小节中，通过利用JPF对同一个等价变异体TriType（int c， int b， int a）的五组不同输入域的检验，说明了运用切片技术对构件系统中单个接口函数的等价变异体进行压缩后，依然能够通过“基于模型检验技术的接口变异测试方法”对等价变异体进行有效地判定。但是，当同一个构件中所有不同的接口函数在分别运用切片技术对构件系统模型进行压缩后，上述实验结果并不能够说明切片技术对整个构件系统的验证以及对接口测试用例生成所产生的影响。因此，本小节将就这一问题作进一步的讨论。
这里，分别以三角形问题构件中的三个状态属性作为兴趣点对构件系统进行切片，然后三个接口函数的非等价变异体对切片后的构件系统模型进行变异并验证。表4给出了三个接口函数在切片前后进行变异并生成测试用例的相关验证信息，为了能够达到对系统模型状态空间进行穷尽搜索以及对非等价变异体生成所有测试用例的目的，这里将JPF中的搜索配置策略设置为“搜索显示多条反例路径”。同样地，表3所产生的状态数也是由统计信息“states”中“new”与“visited”相加得到的。
通过对表3可以发现：
首先，对于每一个需要验证的系统模型来说，在运用切片技术对系统模型进行切片之后，都能够达到压缩系统模型状态空间数量，并提高验证效率的目的。
其次，表中的数据以及实际的实验结果说明，切片后的系统模型在验证后所产生的反例路径与切片之前所产生的反例路径是相同的，因此，切片前后所产生的测试用例也是一样的。
最后，尽管切片技术是对构件系统的功能依赖图进行切片，但其实质上是对构件系统的状态空间进行缩减。由于三角形构件系统中仅由一个三角形构件组成，因此其状态空间是由三边的输入域所确定，这样，表中三组实验所对应的切片前的构件系统模型在验证后所产生的状态空间总数是一样的；同时，对于每一个切片后的构件系统模型来说，其状态空间是由三角形构件中的一个状态所决定的，而该状态又是由相同的输入域确定，因此在切片后，构件系统模型的状态空间总数也是一样的。综上所述，三组实验的状态空间压缩率也是相同的。
3 结束语
目前，基于模型检验的测试用例生成技术作为一种新兴的软件测试方法已经得到了测试人员的广泛关注，但是由于模型检验技术中所存在的“状态空间爆炸”问题会使得验证的效率较为低下，因此，本文主要讲解了运用切片技术对系统模型进行切片从而达到压缩系统模型状态空间，并提高验证效率的目的。
本文以构件之间接口的交互关系为基础，通过扩展构件之间接口交互图后，提出了一种建立构件系统的功能依赖图的具体方法，然后运用切片算法实现了对其进行切片的目标。最后，本文通过基于模型检验的接口变异测试方法对三角形问题的JavaBean构件的实验说明：在运用切片技术对系统模型进行切片以后，达到了有效压缩系统状态空间数量并提高验证效率的目的，同时，不但可以对等价变异体模型进行正确地判定，而且对于非等价变异体模型来说还可以正确地生成测试用例。
参考文献：
[2] 梁陈良， 聂长海， 徐宝文， 陈振宇. 一种基于模型检验的类测试用例生成方法[J]. 东南大学学报（自然科学版）， 2007， 37（5）： 776-781.
[3] W. Visser， C. Pasareanu， S. Khurshid. Test Input Generation with Java PathFinder[C]. Proceedings of ISSTA 2004， New York： ACM Press， July 2004， 97-107.
[4] 李必信. 程序切片技术及其应用[M]. 北京： 科学出版社， 2006： 3.
[5] 张K， 王[， 韩柯， 欧阳志强. 面向构件接口变异的模型检验技术研究[J]. 电脑知识与技术， 2010（6）： 1954-1956.
[7] 李赋欣. 规约和切片技术在组件测试用例生成中的研究[D]. 重庆： 重庆大学， 2007.
[8] 曹严元， 张为群. 一种基于CBD的软件测试方法[J]. 计算机科学， 2005， 32（2）： 156-158.
