基于转换的Java压力测试方法及其应用

理论计算机科学电子笔记174（2007）99-114www.elsevier.com/locate/entcs基于模型驱动转换的Java压力测试Victor L.冬季1，2美国内布拉斯加大学奥马哈分校计算机科学系摘要本文描述了基于转换的分析和代码生成的实际应用。概述了一种自动构造Java压力测试的方法，其执行练习所有“有趣的”类初始化序列的可能性，为一个给定的关键词：程序转换，策略编程，Java类初始化，clinit>方法，JVM，TL，HATS1概述本文描述了一种模型驱动的方法，在该方法中，转换可以用于自动生成Java压力测试，其规模和复杂性抵抗手动构造。该方法由一个框架组成，在这个框架中，可以在不同的抽象级别上对各种Java实体进行建模。所提出的模型具有自然地适合于基于变换的操纵的结构特性。在这种设置中，基于转换的分析是在模型的最抽象形式上执行的，并且基于转换的生成的目标是导出对应的具体模型（即，一组Java类）。本文中讨论的所有分析和生成转换都已使用HATS系统[7]在高阶转换语言TL[8]中实现。由此产生的压力测试被用来帮助验证SSP [6]，一个重要的JVM子集的硬件实现，符合Java虚拟机（JVM）的规范。1这项工作得到美国能源部根据合同DE-AC 04 - 94 AL 85000提供的部分支助。桑迪亚实验室（Sandia）是一个多项目实验室，由洛克希德·马丁公司下属的桑迪亚公司为美国能源部2 电子邮件地址：vwinter@mail.unomaha.edu1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.022100V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99在本文的上下文中，（压力）测试是一组在编译之后，可以作为JVM实现的“输入”。这个测试程序的正确执行提供了一个证据，证明一个实现的某一部分特别是，本文重点关注压力测试的生成，这些测试可用于帮助验证JVM实现在类初始化方面的行为。更具体地说，我们有兴趣提供保证，方法被适当地排序（即，在程序执行期间的适当时间被调用）。本文的其余部分如下：第2节提供了类初始化的背景第3节描述了与我们的测试目标相关的各种模型和模型表示。第4节讨论了测试的选择、观察和生成。本节介绍了识别网的概念，以捕获有趣的临床试验的概念。接下来，给出了一个设计，该设计使得clinit>方法排序能够在测试程序的上下文。然后讨论基于转换的测试生成第5节讨论了如何使用高阶转换语言TL生成初始压力测试。第6节介绍了一些结果，第7节总结。2背景：Java类类初始化是JVM链接阶段的一部分[3]。在Java中，类的初始化在执行期间最多发生一次。我们在验证和准备已经发生的地方开始讨论类初始化。此外，这里我们只描述了用户定义类初始化的一般情况。例如，我们不考虑由于调用各种反射方法而触发的类初始化，例如可以在类Class或包java.lang.reflect中找到的方法。 我们也不讨论与接口相关的初始化最后，由于空间限制，因此，本背景讨论不涵盖常量字段和类的被动使用对类初始化的影响。一般来说，类初始化包括执行与类关联的clinit>此方法由编译器生成，包含实现所有类变量初始值设定项和静态初始值设定项的代码。从从操作的角度来看，类变量初始化器和静态初始化器按照它们在类中语法上出现的顺序执行。clinit>方法不能直接在源代码级别调用，而只能由JVM内部调用，以响应类的第一次活动使用有三种情况构成了类的主动使用：（1）当类的静态字段被访问时，（2）当类的静态方法被调用时，（3）当类的实例被创建时。在字节码级别，有四个字节码，它们的执行构成了对类的主动使用：new，getstatic、putstatic和invokestatic。V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99101规则1：clinit>方法最多只能被调用一次。规则2：类B的clinit>方法必须在B的任何活动使用被评估之前被调用。规则3：在执行类B的clinit>方法体之前，<必须调用B的超类的clinit>规则4：当遇到（在其主体中）一个clinit>方法尚未被调用的类Bk的活动使用时，Bi的clinit>方法规则5：被挂起的clinit>方法（对于类Bi）的执行必须在导致挂起的clinit>方法（对于类Bk）完成后立即A1级intx = A2.w;}class A2 extends A1{ static int w = 1;int x = 0;}class B1{ static int x = B2.w;}public int findDuplicate = 1;int x = b1;}在Java程序执行过程中，一个给定类的clinit>方法最多只能被调用一次。clinit>方法的内部结构（即，它的主体）对于这个讨论来说是重要的，只是在主体可能包含另一个类的有效使用的如果B的超类的clinit>方法没有被调用，则类B的clinit>方法体的执行应该被挂起3.clinit>方法体的执行也应该被挂起，如果在方法体中试图评估一个clinit>方法还没有被调用的类的活动使用挂起方法的执行必须在触发挂起的类的clinit>Fig. 1. 类初始化规则图二. 规则3和规则4最后，B类的积极使用可能会在评估后的任何时间进行评估。<已调用B的clinit>方法（即使B的clinit>方法可能尚未完成）。这种对活动用途的评估的放松提供了一种用于解决clinit>方法之间的循环依赖性的简单方法，从而确保初始化序列是有根据的。3接口的初始化不需要初始化它的超接口，只需要执行接口102V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99图1给出了一组足以确保类初始化正确性的规则。图2突出显示了初始化规则3和初始化规则4之间的区别。特别是，假设A1还没有初始化，第一次主动使用A2.x将导致A2.x被初始化为0。相反，假设B1还没有初始化，第一次主动使用B2.x将导致B2.x被初始化为值1。3概念和术语我们使用术语模型，通常在前面加上描述符（例如，类模型）来表示各种Java实体。模型可以在不同的抽象层次上有表示-有两种表示形式特别有趣：我们使用术语抽象形式来指代我们希望考虑的模型的最抽象的表示。我们使用具体形式这个术语来指代以Java语法表示的模型，这些模型可以合法地嵌入到特定的Java源程序中，编译并执行。我们讨论的范围包括以下模型：• class hierarchy在其抽象形式中，该模型被表示为抽象类模型的列表。在其具体形式中，该模型被表示为具体类模型的列表• 类模型-在其抽象形式中，该模型被表示为以下形式的重写规则[B1→B2B3···Bn]其中B2是B 1的超类，B3···B n表示在B 1的clinit >方法中发生的活动使用序列<。该模型的具体形式如图4所示。具体形式假定<表达式>是对应于B3···Bn的主动使用模型的具体形式。• 主动使用模型（active use model）在其抽象形式中，这个模型被表示为类标识符的列表：B1B2···Bm。在其具体形式中，该模型被表示为以下形式的表达式：（B 1.x + B 2.x +···+ B m.x）其中假设B1，...，B m包含整数标识符x的静态声明。• 观察序列模型在其抽象形式中，这个模型被表示为类标识符的列表：B1B2···Bk。在其具体形式中，该模型表示为：V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99103类的观察结果如图4所示。• 初始化序列模型方法应该根据JVM的规范，为给定的（类层次模型，主动使用模型）对完成。在其抽象形式中，该模型表示为类标识符B1B2···Br的列表。在其具体形式中，该模型由以下布尔值表达式表示：（observe.B 1 == 1 observe.B 2 == 2··· observe.B r == r）其中假设包含类的观测序列模型B1B2···Br存在。4测试：选择、观察和生成我们的测试目标是生成一个Java源程序，该程序可用于验证JVM的实现是否具有符合图1中规则的行为属性。使用上一节定义的概念，抽象形式的测试被建模为一个元组（M，a seq），由类层次模型M和活动使用序列a seq组成。压力测试被建模为测试模型的列表。对于给定的类层次模型M，通常可以构造活动使用序列的无限集合（例如，B，BB，BBB，.）因此，测试（M，B），（M，BB）的数量是无限的，以此类推。然而，由于M是有限的，因此可以论证只有有限数量的“有趣的”活跃使用序列。例如，有人可能会认为，主动使用序列AA是多余的，因此不感兴趣。这样的论点反映了关于测试希望揭示的错误的性质的假设，这些假设有时是微妙的。4.1选择：歧视网络我们说一个主动使用模型对于一个给定的类层次模型M是完备的，当且仅当它保证M中的每个类的初始化，无论是直接的还是间接的。如果（1）类标识符最多出现一次，并且（2）seq不包含完整的适当前缀，则活动使用模型seq的抽象形式是最小的我们将所有最小活跃使用模型的集合称为歧视网。图3以图形形式显示了类层次结构及其鉴别网属于区分网络的抽象主动使用模型是通过连接树中从根到叶的所有路径的类标识符来构造的：{ABC，AC，BC，C}。我们感兴趣的是构造压力测试，对于给定的类结构模型M，该压力测试将验证属于M的区分网的所有活跃使用模型。104V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99A类{static int i = 0;}class B extends A{ static int y = 0;}class C{ static int y = B.y;}A B CB C CC图三. 一类层次结构及其判别网类模型模板class B_i [extends B_r] {static intx = expression>;public intfindDuplicate（）;}观察序列模型模板class observe {static intn;public int findDuplicate（）{Duplicate =Duplicate;returnB_1; returnB_1;}//对于剩余的类B_2，.，B_n//所有set方法使用的位置计数器staticintnext_position=1;}序列模型模板class set_and_check {static inta_seq = B_1.x + B_2.x;//测试序列staticvoid check（）{System.out.println（系统输出.打印ln（打印输出.B_j1== 1&&B_j2 == 2&&...observe. bn == n）;}}测试驱动程序模板class test {publicstatic void main（String [ ] args）{ set_and_check_1.check（）;set_and_check_2.check（）;...set_and_check_m.check（）;}};见图4。混凝土模板V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）991054.2观察<临床>方法排序类之间的clinit依赖关系可以看作是一个有向图结构.这些依赖关系可以通过类层次模型M来建模。给定一个clinit依赖描述M，我们感兴趣的是以具体的形式创建类的层次结构{B1，B2，.，Bn}的依赖关系对应于M。属于类层次结构M的测试类Bi将具有符合图4所示的类模型模板的具体形式。类定义的extendsBr部分是可选的，并且仅在依赖图描述D需要时才包括。在类Bi中，变量x被分配给一个表达式，该表达式的求值显式地触发D调用的活动使用序列。在在这一讨论中，我们将使用Bj1.x + Bj2.x +.的表达式。+ B jk.x，以将活动使用序列Bj 1，Bj2，.，B jk. Bi类中的第二个语句是变量pos的静态声明，其值被赋给observer.setB i（）。这个变量的值表示类的clinit>方法在类层次结构的整个类初始化序列中的位置<。 如果pos的值为零，则我们推断类的方法尚未被调用（或未完成）。对于给定的类层次结构{B1，B2，...， B n}，我们构造了一个关联类观察器。类observe由整数和方法声明组成，其目的是定位记录<{B1，B2，...，Bn}被调用。 注意，B i的clinit >方法的位置的记录<是在Bi外部完成的（即， 在课堂上观察）。 这允许我们以后以一种本身并不构成对Bi的主动使用的方式来查询Bi在clinit序列中的位置。observe类包含与类层次结构中的每个类Bi对应的整数和方法声明，并且具有符合图4所示的观察序列模型模板的结构。对于每个类层次结构{B1，B2，...，B n}，也有一个相关的类集和检查。set和check中的第一个语句是变量seq的静态声明，其初始化表达式由要测试的特定初始（顶级）活动使用序列组成。第二个语句是一个方法检查的声明，它访问类的位置元素，观察类B1，B2，...，B n符合从seq的求值中得到的正确的类初始化序列。类set和check有一个结构符合图4所示的初始化序列模型模板。由于方法只被调用一次，因此在任何给定的执行运行中，类{B1，B2，.，B n}只能用于测试单个活动使用序列的行为。然而，对于给定的（固定的）通过复制类层次结构以及相关的观察、设置和检查类，可以在相同的执行运行中测试类层次结构。可以使用标准的重命名技术来制作这样的副本。 通过这种方式，可以从测试套件的主方法创建并执行一组测试106V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99(1) MA（MA，{aseq1，.， aseqn}）（二）（三{（MA，aseqJ），.， （MA，aseqJ）}11nn{（MA，aseqJ，iseqJ），... （MA，aseqJ，iseqJ）}11 1nn n{（MA1，观察1，设置检查1），.， （MAn，观察n，设置检查n）}{test，（MC1，observe1，set check1），.，（MCn，观察n，设置检查n）}调用已创建的类set和check的每个实例的check方法。这个驱动程序方法的模板如 图 4 所 示 。 注 意 ， 调用set和checki.check （） 将触发set 和check i的方法的执行，这将导致变量set和check. a seq的初始化。4.3的测试生成器设MA和MC分别表示类层次模型的抽象形式和具体形式。 令{aseq1，...，aseq n}表示M A的判别网。 设等式j不表示由（MA，aseqj）实现的（相关）分类初始化等式，并且let（MA，aseqJ）denotea cns是（M A，a s e q j）的tent erenam ing。如果他是个混蛋-JJ需要执行的转换步骤可以总结为如图5所示。图五. 转型步骤在步骤（1）中，使用抽象模型MA来构造判别网{aseq1，.， aseq n}. 在步骤（2）中，通过将抽象模型配对来构造元组其中一致地重命名鉴别网和元组元素中的每个元素。在步骤（3）中，对每个元组（M_A，aseq_J）执行分析，得到JJ期望的初始化序列iseqJ。在步骤（4）中，使用对（aseqJ，iseqjj j j为了生成类的实例，设置并检查，并且模型MAj用于生成一个类observe的实例。最后，在步骤（5）中，转化为具体形式，并增加了驱动类测试。5实践中的转型测试生成器中的许多转换步骤都很简单，由于空间的考虑，没有给出它们实现的具体细节。但是，基本转换的突出显示如图6所示。除了各种标准的转换问题之外，在以本文描述的方式生成Java压力测试时，还必须克服三个主要的转换问题首先，需要定义转换能够为给定的模型M A构造一个判别网。 第二、需要定义能够构造由模型/激活序列对（MA，aseq）暗示的期望初始化序列iseq的第三，必须开发能够在压力测试中一致使用标识符名称的转换（例如，在main方法中调用V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99107类模型转换[B1→B2B3···Bm]=n class B1 extends B2{ static int x =B3···Bm; }=10 class B 1 extends B 2{static int x =（B 3.x +. + B m.x）;}序列转换B1···Br=静态无效检查（）{B1···Br}publicvoid run（）{System.out.println（observe.B 1==1.&B r==r）;}测试类转换class set and check 1{...public void run（）{-你好个文件夹....class set and check s{.public void run（）{-你好个文件夹=公共静态空main（String[] args）{set and check 1.check（）;. set and check s.check（）;}见图6。 转型亮点setand check.check（））。在下一节中，我们将简要介绍TL。然后讨论这三个问题中的两个的实现细节：初始化序列计算和名称的一致使用。5.1TL概述本节简要介绍TL，一种支持各种策略操作符和通用遍历的标记条件（高阶）重写语言有关TL的更详细讨论，请参见[8]。在TL中，解析树是TL程序转换的“对象”。重写规则具有以下形式：r：lhs→sn[if条件]（1）在这个例子中，r表示规则的标签，lhs表示描述树结构的模式，sn表示其评估产生n阶策略的策略表达式，并且if condition表示由使用布尔连接词构造的一个或多个匹配表达式组成的可选布尔值条件模式是一种描述被操作的解析树结构的符号。这种表示法包括在特定树结构域上量化的类型化变量stmtid1= 5）是一个树，根stmt和叶子id1、=和5。在这种情况下，下标变量id1表示在所有以id作为根节点的树的域一般来说一对于BαJ）的部分，在B +α的定义中，根据文法是可能的，并且αJ通过下标所有在α中出现的非终结符。策略表达式是其求值产生具有特定顺序的策略的表达式。在TL的框架中，模式被认为是一种策略，108V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99订单0.将其输入树变换成另一树的重写规则被认为是阶1的策略（即，一阶规则）。设s1表示一阶策略。则规则lhs→s1表示二阶策略（例如，2），等等。匹配表达式是两个模式之间的一阶匹配。令t1表示图案，可能是非接地的，并且令t2表示接地图案。表达式t1t2表示匹配表达式，当且仅当可以构造替换σ使得σ（t1）=t2时，该表达式计算为真。可以使用布尔连接词{and，or，not}组合一个或多个匹配表达式以形成重写规则的条件combinator是一个定义在策略上的算子两个广泛使用的组合子是：（1）从左到右顺序组合（;），和（2）左偏条件组合（+）。设s1和s2表示两个策略。表达式s1;s2表示s1和s2从左到右的顺序组合。当应用于树t时，该策略将首先将s1应用于t，然后将s2应用于结果。 相反，表达式s1+s2表示s1和s2的左偏条件合成。当应用于树t时，尝试将s1应用于t，如果成功，则返回结果;否则，返回将s2应用于t的结果。在TL中，如果s1和s2都不适用，那么t将不改变地返回。换句话说，在TL中，失败被视为一种身份。这是TL区别于像Alpego [5]和Elan [1]这样的系统TL支持各种标准的通用遍历，例如自上而下的从左到右的遍历，在TL中用关键字TDL表示TL还支持高阶通用遍历的定义和使用非正式地，可以将高阶遍历视为用于动态收集多个策略并将它们组合以形成新策略的机制。常见的高阶遍历是以TDL方式遍历树，应用高阶策略sn+1，并使用+组合子组合得到的阶-n策略在TL中，这种遍历由关键字lcond tdl表示。5.1.1瞬态组合器瞬态组合子是TL中一种非常特殊的组合子。这个组合子限制了一个策略，使得它最多只能应用一次。The “at most once” property瞬变现象为自我修正策略打开了大门。当使用遍历将自修改策略应用于术语时，不同的策略可以应用于在遍历期间遇到的每个术语。例如，令r1：int1→int<$2）表示将任意整数重写为值2的规则。如果这样的规则以自上而下的方式应用于项t，TDL{r1}（t），则该项中的所有整数将被重写为2。现在考虑下面的自修改瞬态策略r2：r2：transmant（int1→int<$1））+transmant（int1→int<$2））+transmant（int1→int<$3））V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99109modellist：：= list“;”模型列 表 |єlist：：= item ["+”|““]&& list |єitem：：= class model|......这是什么？classmodel：：= class id|标记类|抽象类|具体类|......这是什么？classid：：= Id标记类 ：：=抽象类：：=具体class：：=...当以自顶向下的方式应用于项t时，TDL{r2}（t），该策略将重写遇到的第一个整数为1，遇到的第二个整数为2，遇到的第三个整数为3。所有其他整数将保持不变。5.2顺序计算确定给定类层次结构的初始化序列和活动使用序列的基本思想如下：被视为堆栈，其中顶部元素Bi表示当前活动的类的clinit>方法。当前活动的clinit>方法Bi由以下(i) 标记：Bi被标记为已被调用。从概念上讲，这是通过重写形式Bi→[Bi]来实现的。(ii) 暂停：Bi暂停。 这是通过将与B i相关联的活动使用模型推到堆栈顶部（通过附加转换）来实现的。(iii) 移除：用于完成步骤1和2的这种移除是通过瞬态组合子完成的。(iv) ：创建一个残留的“清理”转换，删除所有未标记的Bi实例。见图7。 一个扩展的BNF文法片段。图8显示了实现前面段落中描述的转换的TL策略。定义要转换的模型表示的语法结构的上下文无关语法片段如图7所示。在图8中，策略compute iseq是一个高阶策略，当给定类层次模型（listM）和活动使用序列（listaseq）的抽象形式时，它将把listaseq转换为相应的类初始化序列。这种转换是通过应用rm obj<策略来实现的;process[listM]使用遍历TDFIX列出一个seq，如以下策略表达式所示：TDFIX{rm obj<;process[listM]}（listaseq）（2）通用遍历TDFIX是用户定义的，并且正如它在计算iseq中使用的那样，它将对listaseq执行一次自顶向下的遍历，并将策略rm obj<;process[listM]应用于遍历过程中遇到的每个术语110V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99def TDFIX s = TDL{FIX{s}}append：.rm obj：list<$OBJ list2）→list2mark：abstract class<$[IdA→list1]）→list<$IdA list2）→（append[list1]（list<$[IdA]list2）suspend：abstract class<$[IdA→list1]）→list<$[Id A] list2）→（append[list1]（list<$[IdA]list2）cleanup：abstract class<$[IdA→list1]）→list<$IdA list2）→list2标记挂起清理：抽象类A→（transient（mark[abstract classA];suspend[abstract classA]）<+abstract class A[abstract classA]）进程：lcond tdl{标记挂起清理}计算公式：listM→listaseq→TDFIX{rmobj<;process[listM]}（listaseq）见图8。确定类初始化顺序（注意，策略rm obj将从我们的初始化序列模型中删除所有出现的OBJ。这样做的原因是我们没有对类Object的行为建模。如图所示，process是一个二阶策略，当应用于类层次模型（列表M）时，它将产生一个策略，该策略为列表M中的每个类建模clinit>方法的clinit排序规则。更具体地说，process通过遍历列表M并应用策略标记suspend cleanup来实现这一点对遇到的每个抽象类，并使用+组合子组合得到的一阶5.3名称的一致使用当生成压力测试时，围绕名称一致使用的问题是分布式数据问题（DDP）的一个实例[8]。 当语义关系存在于句法上不相关的术语之间时，DDP出现。在实践中，这意味着信息（例如，要引用的标识符名称）必须使用除编码传递匹配或统一之外的机制在术语之间显式地传输。转换的参数化是一种通常用于处理DDP的标准方法。其他方法包括（1）在一阶[4]或高阶设置[8]中动态创建重写规则和策略，以及（2）可以组合数据和计算的期限结构的融合[2]。在本文描述的转换中，通过（1）适当选择标识符名称，以及（2）一致使用单个模型来导出压力测试的各种组件，避免了DDP的 例如，在observe类中，integer被声明为对应于每个类，我们希望其clinit行为观察。然后在方法检查中引用这些监视变量V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99111收集设置并检查：id1→transient（list1→list<$id1.check（）;list1））ifid1wild id<$set and check（）make test class：型号列表1→型号列表<$型号1;型号列表1）如果list1TDL{lcondtdl{collectsetanddcheck}[modellist1]}（list <$））anddmodel1modellastest{publicstaticvoidmain（String[]args）{list1}}）这是伴随类设置和检查的一部分。因此，在observe类中声明监视标识符和随后在方法检查中使用它们之间存在关系。在这种情况下，只需选择监视标识符的名称，在语法上与它们要监视的类的标识符相同（例如，C类的监控标识符将是C）。 给定这种方法，可以直接从模型MAk中导出类observe、set和check的一 致版 本。类observe中的set方法为我们的方法添加了一个小小的皱纹。理想情况下，我们希望有一个函数来生成具有以下输入/输出行为的新标识符名称：special new（B k）= setB k像special new这样的生成器可以用来在observe中生成方法声明，在set和check中生成相应的方法调用。请注意，函数special new除了能够从两个其他标识符的连接中生成标识符令牌之外，没有什么值得注意的。在TL中，这样的函数可以很容易地定义，放在用户定义的库中，在一个transformation中可以创建类似的函数来生成类observe、set和check的实例（例如，标识符观察与类层次模型中出现的第一个类标识符连接，以创建类观察的唯一实例）。DDP的另一个例子是需要从驱动程序类测试的main方法中调用所有检查方法。在这里，TL承认一个新的解决方案，利用在令牌级的关联匹配。具体来说，TL允许构造包含一个或多个由符号“”表示的“”的出现的标识符模式。在TL中提供这种功能的最初动机是为了方便在AOP环境中编织期间执行的各种转换-特别是AOP J切入点描述符。然而，正如我们在这里看到的，这种能力也有其他用途。图9.第九条。 在测试驱动程序的构造中使用匹配图9显示了用于构造驱动程序类测试的转换。策略性试题中策略性表达的评价6结果lcond tdl{收集设置和检查}[模型列表1]（3）112V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99抽象模型（输入）总数类数量测试组[A→OBJ]214【B→A】【C→B】[A→目标B]8512【B→A】[C→D A][D→A B C][E→C][A→OBJ]50563[B→A C][C→目标A][D→OBJ][E→D B][F→A B C D E][A→OBJ]2401240[B→A C][C→目标A][D→目标B][E→D B][F→A B C D][G→OBJ A F][H→G F A]见图10。 电子邮件生成的压力测试将遍历模型列表1中的测试，并为类的每个实例生成策略瞬态的实例（列表1→列表ID1.check（）;列表1）V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99113遇到的设置和检查。在提出的解决方案中，set和check的实例是通过连接一个唯一的suprix来设置和检查的（例如， 设置并检查01）。在规则的条件部分收集set和check，set和check的实例是承认通过的通配符匹配id1wildid设置并检查id）。transmant 的 结 果 实 例 （ list1→list<$id1.check （ ） ;list1 ） ） 用 于 填 充 术 语list<$）这是使用自顶向下遍历TDL完成的。然后将结果列表放置在主类测试的方法。图10给出了为几个抽象模型生成的压力测试的度量，这些抽象模型用作测试生成器的输入。在第4.1节中，我们给出了将我们在测试生成中的注意力限制在最小的主动使用序列的理由。这限制了可以为给定类层次结构生成的测试数量。例如，包含n个类的层次结构最多可以有n个类。在其歧视网络中进行测试。当层次结构中的所有类都有一个形式为[Bi→OBJ]的抽象模型时，就会出现这种情况。在另一个极端，最小的鉴别网将具有大小n。这种情况发生在层次结构中的依赖关系是这样的，任何类的第一次活动使用将导致层次结构中所有其他类的初始化。7总结和结论压力测试可以为系统的保证论证做出重大贡献。压力测试的规模和复杂性常常使其手动生成变得不切实际。自动生成压力测试时面临的两个主要挑战是：（1）开发用于选择测试用例的系统方法，以及（2）构造可用于自动检查测试用例结果的证书。在本文中，我们已经提出了一种方法，用于clinit测试生成的测试用例的选择和生成的certificates发生在一个抽象的形式的模型和结果，然后转化为具体的测试。引用[1] P. Borovansky'，C. Kirchner，H. Kirchner，P. -E. 莫雷奥和C。 Ringe is e n. 一个新的生活。 Electr.注意Theor。Comput. Sci. ，15，1998。[2] R. 我是说我和J。 Vi ss er. AStrafunskiApplicationLetterr.在V。 达兰和P。 我是说，我的意思是。的Practical Aspects of Declarative Programming（PADL'03），LNCS的第2562卷，第357-375页。施普林格出版社2003年。[3] T. Lindholm和F.耶林，编辑们。 Java虚拟机（第二版） Addison-Wesley，1999年。[4] K. O. M. Bravenboer，A. van Dam和E.维瑟使用限定作用域的动态重写规则进行程序转换。技术报告UU-CS-2005-005，信息和计算科学研究所，乌得勒支大学，2005年。[5] E. Visser，Z. el Abidine Benaissa和A.托马赫用重写策略构建程序优化器。在ICFPACM Press，1998.114V.L. Winter/Electronic Notes in Theoretical Computer Science 174（2007）99[6] G. L. Wickstrom，J. Davis，S. E.莫里森，S。Roach和V.L. 冬天SSP：一个例子高可靠性系统工程2004年，第八届IEEE高保证系统工程国际研讨会.[7] V. Winter和J. Beranek。使用HATS进行程序转换。软件工程中的生成和转换技术（GTTSE），第95-111页[8] V. Winter 和 M. Subramaniam 动 态 策 略 、 瞬 时 策 略 和 分 布 式 数 据 问 题 。 Science of ComputerProgramming（Special Issue on Program Transformation），52：165-212，2004.