Java测试套件覆盖率的JML规格衡量方法及工具介绍

理论计算机科学电子札记190（2007）21-32www.elsevier.com/locate/entcs使用以下工具测量Java测试套件覆盖率JML规格F. Dadeaua，1，4 Y.Ledrua，2 L. du Bousqueta，3aGrenobleBP72，38402SaintMarrtind摘要在本文中，我们提出了一种方法来衡量覆盖率的Java测试套件，考虑JML规格相关联的Java程序测试。这种方法基于从JML方法规范中提取基于谓词的图。 然后，我们测量后一种w.r.t. 节点测试套件所访问的图形的。此外，我们建议检查测试套件是否满足经典的条件覆盖标准。 我们还介绍了一个工具，用于Java的预编译器，这是负责测量和报告的覆盖率根据这些标准。保留字：规范覆盖率，测试套件，Java，JML，条件覆盖率。1引言测试的本质在于执行被测系统以发现bug [21]。然而，测试不能是一个完整的方法，因为详尽的测试是不适用的;验证工程师经常留下一个测试套件，没有检测到任何程序中的错误。他/她如何确保运行的测试套件足够相关，可以在程序中确信？一个解决方案是评估测试套件的质量。测试套件评估的几个工作存在，如行使测试套件的程序的突变。最相关的技术是测量测试套件的覆盖率。通常，覆盖率是在程序的控制流图上测量的[21]，或者在程序的数据流上测量的[24]。此外，可以测量特定覆盖范围。1 电子邮件：Frederic. imag.fr2电子邮件：Yves. imag.fr3 电子邮件：Lydie. imag.fr4这项工作得到了法国研究和新技术部支持的RNTL POSE项目（ANR-05-RNTL-01001）的部分资助。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.00322F. Dadeau等人/理论计算机科学电子笔记190（2007）21最近出现的注释语言使得在源代码中指定程序（即方法）的前置条件和后置条件成为可能。它提供了方法应该做什么的另一个它还提供了一个方法应该做什么的黑盒视图，以合同的形式表达[20]。基于模型的测试[2]包括从所考虑的程序或系统的模型计算测试套件。基于模型的一致性测试包括确保程序没有意外的行为w.r.t.其规格。这种一致性可以通过观察点或使用运行时断言检查机制来观察，如果规范和程序的接近性使其成为可能。在这种情况下，Java建模语言[16]（JML）被引入作为Java程序的行为接口规范语言（BISL）。JML可以用作测试的预言机，考虑到如果在程序执行期间没有违反JML断言，则测试成功，否则测试失败。以前的工作[3]已经从JML规范中介绍了基于模型的测试的原则。因此，一些基于JML的覆盖标准被用来指导测试目标的定义。 我们得出的想法是，在后一项工作中定义的覆盖标准可以用于评估测试套件，这些测试套件可以由几种工具使用不同的方法（如组合测试）(e.g.JMLUNIT[6]，TOBIAS[18]）或随机测试（例如JARTEGE[23]）。我们提出了一种方法来评估测试套件的Java程序w.r.t.相关JML规范的覆盖范围，表达方法的行为和/或要求。此外，我们建议检查不同的条件覆盖标准，这些标准包含在指定谓词的析取中。本文的结构如下。第2节介绍了Java建模语言提供的建模基于方法规范的第一个覆盖标准见第3节。第4节专门讨论条件覆盖定义。第5节详细介绍了措施的原理，特别是实施和实验。第6节介绍了相关的工作，然后总结并简要介绍了第6节的未来工作。7 .第一次会议。2Java建模语言Java建模语言Leavens等人在爱荷华州立大学[16，17]。建模元素显示为注释，嵌入在Java源代码中。JML基于契约设计原则（DBC）[20]，该原则指出，在调用方法时，系统必须完成一个契约（通过满足方法JML使我们能够使用后置条件和历史条件来表示系统的静态部分（如不变量）和系统的动态部分F. Dadeau等人/理论计算机科学电子笔记190（2007）2123publicclass Monkey{静态最终SET_MAX_DEBIT =1;静态最终SET_MAX_BAL =2;//@invariant balance>= 0&&//@ balance<= maxBal;intbalance，maxBal，maxBal;布尔个性化;/*@ behavior@ requires personalized==false;@{|@需要p1 == SET_MAX_DEBIT;@需要数据>=0;@assignablemaximum，maxBal;@确保maximum==data&&@maxBal ==\old（maxBal）;@also@需要 p1== SET_MAX_BAL;@requires data>=balance;@assignable maximum，maxBal;@确保maxBal ==data&&@马克斯==\new（）;@|}@也@requires personalized==true||@（（p1！=SET_MAX_DEBIT||@数据< 余额）&&@（p1！= 设置最大值||intmaximum（）;<@assignable maximum，maxBal;@确保false;@signals（CardException e）@maximum ==\old（maximum）@maxBal ==\old（maxBal）; @*/public void PUT_DATA（bytes p1，shortdata）;...}图1. 一个JML规范约束。该模型通过几个子句来表达，由关键字标识，后跟谓词。不变和约束子句分别指定应用于类的不变和历史约束。方法的一般行为通过方法规范来指定，方法规范包含由also关键字分隔的规范块。 每种规格块显示前置条件（requires子句），正常后置条件-已建立当方法终止时，没有抛出异常一个例外可赋值子句给出了方法的框架。JML谓词语法类似于Java谓词语法，它富含特殊的关键字，前缀为\，特别是引入了quantifier（\forall，\exists）。图1显示了JML规范的一个示例。该规范提出了Demoney电子钱包的简化版本[19]。属性balance、maxBal和maxBal分别表示钱包中的金额、最大金额和授权的最大借方。最后，属性个性化通过定义后两个属性的值来这里显示的方法可以通过设置余额的最大值或最大借方来配置钱包。如果参数p1是错误的，或者如果卡已经被个性化，则该方法可能抛出异常。开发JML断言查询（RAC）[5]是为了检查运行程序时的JML规范子句。这个工具在JML发行版中提供，作为一个预编译器，它修改程序的源代码，以在JML模型上添加以下验证：（i）在输入方法时检查前置条件和不变量，（ii）捕获可能抛出的异常，并在再次抛出异常之前检查与所考虑的异常相关的异常后置条件，（iii）如果方法正常终止，则检查正常后置条件。请注意，在步骤（ii）和（iii）中还检查了不变和历史约束。24F. Dadeau等人/理论计算机科学电子笔记190（2007）21下一节介绍我们将JML方法规范分解为行为的建议，行为的覆盖率是我们方法的度量单位此外，我们将考虑条件覆盖标准，这将为度量增加更多的3方法质量标准方法规范描述了Java方法的行为。如果方法正常终止（没有抛出异常），则行为是正常的，如果方法通过抛出异常终止，则行为是异常的。我们的技术是从方法规范中提取一个基于谓词的图，它给出了方法行为的表示。遍历图等价于在其边缘上创建标签谓词的合取。我们用图表示每个JML方法规范，如图2所示。在该图中，P k（k∈ 1. N）是前提谓词，A给出框架条件，Qk（k∈ 1. N）是正规后置条件，Sp（p∈ 1. M）是例外与异常Ep相关的后置条件。 终止由T来区分，T可能是表示正常行为的无异常，也可能是任何声明的异常Ep。不变量和历史约束（目前）不考虑。/*@ behavior@需要P1;@assignableA;@确保Q1;@signals（E11e11）S11;@.@signals（E1Me1M）S1M;@also@...@也@需要PN;@assignableA;@确保QN;@signals（E N1eN1）SN1;@ ...@signals（ENPeNP）SNP;@*/T甲基（T1p1，. . ）抛出E11，...，E NP{. 个文件夹图2. 从JML方法规范1T=无例外PNP1278P1T=E11T=E1MT=ET=EN1NP3P19 10 .. ... .11...12年q14S11S1MSN15PNSNPPN6QN0F. Dadeau等人/理论计算机科学电子笔记190（2007）2125/*@需要P1;@可赋值A;/*@需要P1||P2;@确保Q1;/*@需要P1 ||P2;@assignable A;@也=@ 可赋值的A;=@确保（\old（P1）Q1）@需要P2;@确保\old（P1）==> Q1;||\old（！P1）;@可赋值的A;@确保\old（P2）==> Q2;@确保（\old（P2）Q2）@确保Q2;@*/||\old（！P2）;@*/@*/图3. JML方法规范块的去糖图的提取如下进行。构建包含正常行为的第一个分支。根据JML的语义，当一个方法规范块的前提条件满足时，则必须建立正常的后置条件。否则，如果前提条件不满足，任何事情都可能发生。这种脱糖[25]可以用图3表示。结果，创建了条件分支，以便重新创建蕴涵。对每个方法规范块进行一次分支在异常终止的情况下，如果抛出异常，则必须根据前提条件建立异常后置条件。图4中给出了这种图的示例。请注意，图中不考虑结构件条件通过覆盖方法规范图实现方法规范的覆盖。由于这个图是有向的和无环的，我们不必覆盖循环。因此，可以提出以下备选方案。- 所有节点当测试套件激活图的所有节点时实现。- 所有边缘。当测试套件激活图的所有边时实现。- 所有路径。当测试套件激活从节点1到节点0的图的所有路径时实现。这些选项之间的层次结构如下：所有节点所有边所有路径我们假设只有一致的路径被计算/测量。这可以通过编写一个全面的JML方法规范来确保，或者通过使用专用工具，如JML-T约束求解引擎[4]或定理证明器，如JML [9]或HARVey [8]来修剪方法规范图中的不一致路径。例3.1[从方法规范中提取图]考虑图1中给出的方法规范示例。图4给出了相应的曲线图。 路径被解读为出现在其边缘的语句的连接。在本例中，path[ 1→ 9→ 10→ 0]等价于XT=CardExceptionmaxBal=\old（maxBal） 这张图展示了在从节点1到节点2的所有可能路径中，0. 在该示例中，仅路径[1→ 2→ 3→ 4→ 5→ 7→ 0]、[1→ 2→ 3→ 5→6→ 7→ 0]和[1→ 9→ 10→ 0]是一致的。图3说明了JML方法规范的去糖化，重写了几个26F. Dadeau等人/理论计算机科学电子笔记190（2007）21\old（personalized）==falseT=无exc12\old（个性化）||（（p1！= 设置最大借方||p1 ==设置最大借方3&&数据>=0X=data<\old（balance））&&（p1！= 设 置 最大平衡||数据0））4maxBal == data maxBal ==\old（maxBal）&&5p1！= 设置最大借方|| 数据<0p1！= 设置最大平衡||数据\旧（余额）9T=CardExceptionp1 ==设置最大平衡值&&data>=\old（balance）6710maximum ==\ old（maximum）！XmaxBal ==\old（maxBal）maximum ==\ old（maximum）&&maxBal == dataX8错误 0图4. 从PUT DATA方法规范将所有的块合并成一个块。图的构造是基于这样的假设，即规格尽可能多地划分为几个块（图的左侧部分）。然而，大多数JML规范编写者并不习惯于像这样拆分规范，而只是编写一个巨大的后置条件，其中基于案例的后置条件被保护（图的中间部分）。因此，这种方法规范的图只考虑一个先决条件和一个后置条件。测量这种图的覆盖率实际上并不重要。这就是为什么，除了谓词图的覆盖之外，我们还考虑图的谓词的条件如果方法规范被划分为块，那么这个额外的覆盖范围增加了我们度量的粒度4条件覆盖条件覆盖是通过重写嵌入在构成路径的边上的谓词中的析取来实现的。我们区分了4种重写，每一种重写都代表一个特定的条件覆盖标准。表1给出了这些重写及其相关的覆盖标准。重写1在于检查析取而不进行任何更改。这是检验析取的最基本的方法，通过选择第一个正字面值。重写2在于独立地考虑每个文字。这种重写满足条件覆盖准则（CC）。重写3以排他性的方式考虑每个文字，通过评估每个文字和其他文字的否定因此，这种重写满足全谓词覆盖标准（FPC）[22]。最后，最后一次重写评估每个可能性以满足析取。这允许满足多条件覆盖（MCC）。F. Dadeau等人/理论计算机科学电子笔记190（2007）2127重写要为P1评估的谓词集||P2覆盖准则RW1{P1||P2}RW2{P1，P2}CCRW3{P1&&！P2，！P1P2}&&FPCRW4{P1&&！P2，！P1P2，P1P2}&&&&MCC表1析取重写和覆盖标准在这里，我们可以再次在重写和条件覆盖标准之间建立以下层次结构。RW1RW 2RW 3RW 4请注意，测量前提条件的覆盖率可以简化为测量前提条件的满足程度，而通常也测量前提条件的不满足程度。由于我们独立地考虑了前提条件的否定，因此通过图的构造，这一步骤是隐式执行的。出于实际原因，所有这些重写仅适用于方法规范块的正先决条件。事实上，这些重写在否定前提条件上的应用将导致对案例数量的组合探索。然而，可以应用RW1或RW2，其可以是测试套件是否尝试执行未授权动作的指示器，以及这些动作尝试被激活的上下文。5执行测量首先，我们介绍了用于执行覆盖测量的原则。其次，我们提出了一个实现这些原则的工具。5.1原则检查JML规范的覆盖率的原理类似于在RAC中执行的断言的运行时检查。它是作为一个预处理来呈现的，它通过JML谓词的验证来丰富原始Java代码。此外，我们需要设置一个覆盖率报告管理器（CRM），专门用于必须执行的措施。CRM跟踪代表每个方法规范的图表。每次在源代码中检查谓词时，报告管理器都会被告知已覆盖的边和已到达的节点。简而言之，该原理在图1中的通用方法规范中进行了说明五、重要的是要注意，对于JML断言，添加到Java代码中的验证一般不会改变方法的功能行为和程序的功能行为。28F. Dadeau等人/理论计算机科学电子笔记190（2007）21CRM中的专用内部方法负责计算测试套件执行结束时实现的边缘/节点覆盖率。可以显示报告或使用自定义API进行咨询5.2jmlCoverage工具jmlCoverage工具实现了前面描述的原理，如图6所示。它充当一个预编译器，生成覆盖率报告管理器（作为Java源文件）和监视器本身，作为一个Ablogj文件或一个插装的Java源文件，负责监视所观察到的方法的执行当主程序执行结束时，覆盖报告管理器显示一个表格，该表格通知JML方法规范图的节点/边/路径的覆盖率，用于可以应用的每个条件重写jmlCoverage是独立于JML运行时断言库开发的该工具支持与RAC相同的功能，因此，它要求JML表达式是可执行的（即，在一个有限的整数范围内存在的\forall或基本上，所有的结构JMLRAC接受的值可以被工具接受。 它的使用独立于虽然这不是RAC的第一个意图，但jmlCoverage也能够检测不是由实现建立的后置条件。下一节将报告在一个实际案例研究中如何使用jmlCoverage5.3实验5.3.1目标程序。我们已经在一个案例研究中实验了我们的方法，该案例研究改编自一个名为Demoney的工业示例[19]。Demoney是Trusted Logics设计的一个小程序，实现了一个电子钱包。为了实验的目的，我们开发了一个简化版本的实现，它以前已经用JML注释来描述其功能行为。应用程序的类表示大约500行JML，分布在4个类中。5.3.2选择测试工具。然后，我们选择了两个（半）自动化测试生成工具，我们想评估测试套件生成能力。我们选择了一个跑步-DOM测试工具，JARTEGE[23]和组合测试工具，托拜厄斯[18]。JARTEGE产生给定数量的序列，每个序列具有给定的长度，并且由使用随机输入的随机选择的方法调用组成。另一方面，TOBIAS能够从定义为正则表达式的测试模式中生成大型组合测试套件。这两种工具都依赖于JML方法规范来过滤不满足方法先决条件的测试用例。F. Dadeau等人/理论计算机科学电子笔记190（2007）2129/*@ behavior@需要P1;@assignableA;@确保Q1;@signals（E11e11）S11;@.@signals（E1Me1M）S1M;@also@...@也@需要PN;@assignableA;@确保QN;@signals（E N1eN1）SN1;@ ...@signals（ENPeNP）SNP;@*/T甲基（T1p1，. . ）抛出. {body;}T甲基（T1p1，. . ）抛出. {检查并报告前提条件边谓词覆盖率尝试{身体;}catch（java.lang.Errore）{if（einstanceofE11）{检查和报告边缘谓词覆盖E1}...if（e instanceofENP）{检查并报告EN的边缘谓词覆盖率}投掷;}检查并报告正常后置条件的边缘谓词}图5. 插装java源代码5.3.3Study.首先，我们在Demoney类上运行JARTEGE。由于JARTEGE是一个随机测试工具，我们有兴趣评估这样一个工具的效率。它的使用表明了我们的方法的实用性，以及对所产生的测试套件的有趣的反馈。事实上，将JARTEGE与jmlCoverage连接起来以提供帮助的可能性似乎是一个有趣的选择。在这种情况下，jmlCoverage可以用来限制生成的测试用例的数量，通过生成测试直到达到用户定义的规范覆盖率。其次，我们设计了5个测试模式，TOBIAS在162个测试用例中展开。由此产生的抽象测试被具体化为Java测试程序。 我们已经能够建立我们的测试方案的整体覆盖范围。在这里，我们的工具可以用来掌握组合覆盖率报告管理器通知监视器（Java或AJAX）图6. 测量规范覆盖率Java/JML源文件30F. Dadeau等人/理论计算机科学电子笔记190（2007）21TS大小×TS数量javacRACjmlCoverageRAC+jmlCoverage100 ×100.7381.3040.7681.244100 ×201.1951.1161.1401.676100 ×502.6711.1651.7112.010100 ×1004.9871.5652.1092.464表2案例研究的执行时间结果（单位：毫秒）由模式的使用引起的爆炸。对于这两个工具，规范覆盖度量对于验证工程师了解测试套件是否相关是一个很好的帮助。一个有趣的地方是测试套件w.r.t.额外的注释。表2显示了几个测试套件w.r.t.在程序上（i）没有任何运行时验证，（ii）有JML断言检查，（iii）有JML断言覆盖度量，以及（iv）有（ii）和（iii）。注意测试套件是使用JARTEGE自动生成的。还要注意，（i）的执行时间可能比其他情况下更长，因为运行时检查可能会显示不确定的测试（即，不尊重一个方法结果表明，无论执行RAC，执行jmlCoverage的成本都很小。这是因为RAC执行的检查比jmlCoverage多得多，因为它系统地检查不变量和历史约束。但是，在RAC之上使用jmlCoverage的额外成本是最小的，即使对于较大的测试套件也是如此。6相关工作JML方法断言库[5]已经能够报告JML方法规范的部分覆盖，表明前提条件是否被覆盖一次，多次或从未被覆盖。尽管如此，它并不呈现与我们的方法相同的粒度，并且不能被视为相关的覆盖率测量工具。VDMTools [11]也采用DBC方法。它们提供了覆盖工具，将前置和后置条件视为普通语句，并衡量有多少指定已被执行。换句话说，它提供了一个扩展的声明覆盖范围的概念，在大多数情况下，它比我们的措施更弱。UML规范的覆盖度量[1]也有研究，特别是基于状态图的结构覆盖。Simulink状态图[12]还能够在状态图上执行模型覆盖测量。测试套件测量的一个补充视图是代码覆盖测量，可以通过JCover [14]，JCoverage [15]，clover [7]或EMMA [10]等工具实现。F. Dadeau等人/理论计算机科学电子笔记190（2007）2131我们提出的方法受到经典控制流图覆盖标准[21]和经典条件覆盖标准[22]的启发。新颖之处在于将这些标准应用于从JML方法规范中提取的基于谓词的图。此外，使用规范覆盖工具而不是代码覆盖的兴趣在于，规范使得可以独立于特定实现来表达属性，从而允许基于程序的黑盒视图进行更具体的测量。7结论和未来工作本文提出了一种通过Java测试套件测量JML方法规范覆盖率的方法。采用运行时断言检查机制来确保从方法规范中提取的图的覆盖率这项工作的独创性是标准的应用JML。我们相信这项工作可以帮助提高验证工程师在他/她的测试套件中的信心从技术的角度来看，使用方面对断言进行运行时检查，使我们不必再请求Java源代码。我们只需要JML规范。因此，这种方法适合于基于模型的测试。本文提出的工作一个定义的覆盖标准，使减少的测试套件提供相同的覆盖作为完整的一个[13]。此外，Java接口对于连接同样用Java编写的JARTEGE可能很有趣有趣的一点是扩展JML规范的覆盖范围，以考虑其他子句，例如类不变式或历史约束。 此外，我们希望将jmlCoverage的开发基于RAC的体系结构。这将增加工具w.r.t.的演变。JML的演变，并且它将使得重用RAC的断言生成机制成为可能。最后，使用注释建模语言（如JML）使我们考虑将这项工作扩展到Spec#规范，这可能不会带来任何困难。引用[1] A. Amschler Andrews，R.B.法国S. Ghosh和G.克雷格uml设计模型的测试充分性准则。软件测试、验证和可靠性，13（2）：95[2] B. 贝泽黑盒测试：软件和系统功能测试技术。约翰威利父子公司，纽约，美国，1995年。[3] F. Bouquet，F. Dadeau和B. Legeard。从JML规范自动生成边界测试。在FM史普林格出版社[4] F. Bouquet ， F. 达 多 湾Legeard 和 M.Utting.JML-Testing-Tools ： a Symbolic Animator for JMLSpecifications using CLP. 在 Proceedings of 11th Int. Conf. on Tools and Algorithms for theConstruction and Analysis of Systems，Tool session（TACAS史普林格出版社[5] Y. Cheon和G.T.莱文斯 Java建模语言（JML）的一个断言。在哈米德河Arabnia和Youngsong Mun，编辑，32F. Dadeau等人/理论计算机科学电子笔记190（2007）21软件工程研究与实践（SERPCSREA Press，June 2002.[6] Y. Cheon和G.T.莱文斯一种简单实用的单元测试方法：JML和JUnit方法。在Boris Magnusson，编辑，ECOOP 2002 -面 向对 象编 程 ，第16 届 欧洲 会议，M′aalag a，Spanin，Proceedings， 第237 4卷，LNCS，第231-255页，Ber lin，2002年6月。史普林格出版社[7] Clover网站http://cenqua.com/clover/，2006年。[8] D. Deharbe和S.瑞妮丝2003年，用于调试和验证代码单元的轻量级定理证明。[9] D. Detlefs，G. Nelson和J.B.萨克斯一个用于程序检查的定理证明器。J. ACM，52（3）：365[10] 艾玛网站 http://emma.sourceforge.net/，2006年。[11]VDM工 具 组 。 用 户 手 册 。 技 术 报 告 ， 农 发 基 金 ， 2000年 10 月 。ftp://ftp.ifad.dk/pub/vdmtools/doc/userman letter.pdf。[12] G. Hamon和 J.M. 拉什比一个 业务 语义为 州议会。In M. Wermelinger和T. Margaria，编辑，FASE，计算机科学讲义第2984卷，第229-243页。Springer，2004.[13] M.J. Harrold，R. Gupta和M.L.所以你要小心点。控制测试套件大小的一种方法。ACM Trans. Softw.工程师，Methodol。，2（3）：270[14] JCover网站。http://www.codework.com/JCover/product.html，2006年。[15] JCoverage网站。 http://www.jcoverage.com/，2006年。[16] G.T. Leavens ， A. L. Baker ， and C. 露 比JML ： Java 建 模 语 言 。在 正 式 的 基 础 上Java 研 讨 会（OOPSLA'98 ） ， 1998 年 10 月 。[17] G.T. Leavens，A. L. Baker，and C Ruby. JML：详细设计的符号。在Haim Kilov，Bernhard Rumpe和IanSimmonds，编辑，企业和系统的行为规范，第175188. Kluwer Academic Publishers，Boston，1999.[18] Y. 莱 德 鲁 湖 du Bousquet ， O. Maury ， and P. Bontron. 过 滤 托 比 亚 斯 组 合 测 试 套 件 。在 MichelWermelinger和Tiziana Margaria，编辑，软件工程的基本方法，第7届国际会议，FASE 2004，计算机科学讲义第2984卷，第281-294页，巴塞罗那，西班牙，2004年史普林格出版社[19] R. Marlet 和C. 梅 斯尼 Demoney ： 一个 演示 性的 电 子钱 包卡 规范 。技 术 报告SECSAFE-TL-007 ，SecSafe，2002年。[20] 伯特兰·迈耶。面向对象的软件构造。普伦蒂斯·霍尔，第二版，1997年. MEY b 88：1 2.P-Ex.[21] 格伦福德·J迈尔斯软件测试的艺术。约翰威利父子公司，美国纽约州纽约市，1979年。[22] A.J.O. Xiong和S.刘某生成基于规范的测试的标准。 在1999年10月在美国拉斯维加斯举行的第5届IEEE复杂计算机系统工程国际会议（ICECCSIEEE计算机学会出版社.[23] 凯瑟琳·奥瑞特。Jartege：一个为Java类随机生成单元测试的工具。第二届软件质量国际研讨会论文集，SOQUA 2005，计算机科学讲义第3712卷，第242-256页，德国Ergoman，2005年9月史普林格出版社[24] 诺伯特·奥斯特。面向对象软件的基于数据流的测试数据的自动生成和评估：Java类单元测试随机生成工具。第二届软件质量国际研讨会论文集，SOQUA 2005，计算机科学讲义第3712卷，第212-226页，德国Ergoman，2005年9月史普林格出版社[25] A.D. Raghavan和G.T.莱文斯脱糖JML方法规范。技术报告00- 03 e，爱荷华州立大学计算机科学系，2005年5月。