没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记190(2007)73-84www.elsevier.com/locate/entcs匹配检验与证据覆盖率Y. Ledrua,1 L. du Bousqueta,2 F.Dadeaua,3,4 F.阿利西亚aGrenobleBP72,38402SaintMarrtind摘要本文研究了Java程序的测试和演绎证明过程的互补性,JML(Java建模语言)程序的证明可能是漫长而困难的,特别是当自动证明器放弃的时候。当一个定理没有被自动证明时,有两种可能性:要么定理是正确的,没有足够的信息来处理证明,要么定理不正确.为了区分这两种选择,可以使用测试技术。 在这里,我们提出的实验,围绕使用JACK工具来证明Java程序注释的JML断言。当杰克未能决定证明义务,我们使用组合测试工具,TOBIAS,产生大型测试套件,行使未经证明的程序部分。关键问题是确定测试集与未经证明的证明义务的相关性。因此,我们使用代码覆盖技术:我们的方法利用语句导向的JACK工具,比较涉及未经证明的证明义务和测试套件所涵盖的语句。最后,我们通过在突变程序杀死练习中评估测试套件来确保我们对测试套件的信心。这些技术已付诸实践,并说明了一个简单的案例研究。关键词:演绎证明过程,组合测试,测试集相关性评估,JML1引言软件测试已经成为评估规范和某些实现之间不幸的是,测试只能揭示错误的存在,而一致性只能通过形式证明、针对某些标准的详尽测试或两者的组合来完全形式证明技术通常很难应用,因为它们中的大多数需要高水平的数学技能。为了使证明技术1电子邮件:Yves. imag.fr2电子邮件:Lydie. imag.fr3电子邮件:Frederic. 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.00774Y. Ledru等人理论计算机科学电子笔记190(2007)73由于非专业人士也可以使用,因此在过去几年中已花费大量精力提供自动演绎证明工具。例如,JACK工具[2]被设计用于自动证明某些Java代码相对于其JML规范的正确性。JML(Java Modeling Language,Java建模语言[9])是Java的一种正式规范语言,基于断言,如不变量,前置和后置条件。在证明过程中,JACK首先产生证明义务,以证明实现(即代码)符合其规范。然后,JACK尝试自动证明它们中的每然而,困难依然存在;当一个定理不能被自动证明时,有两种可能性:要么这个定理是正确的,而证明者不能决定它,要么这个定理只是不正确。在这些情况下,测试可能有助于显示代码(或规范)中存在错误,或增加定理正确的信心(意味着实现符合其规范)。为了实现这一点,我们的建议是产生大量的测试,与组合测试技术。然后,必须评估测试套件的相关性。事实上,如果测试用例与程序中涉及证明义务的部分无关,它们就不能提供关于待证明定理正确性的在这项工作中,测试套件的相关性进行评估覆盖测量。第2节介绍了JML的原理,JML是一种可执行的基于模型的规范语言。第3节概述了JACK证明器。第4节描述了测试过程,并简要介绍了TOBIAS工具。第5节和第6节分别使用覆盖和变异技术对测试集的质量进行了评价。第8章得出结论,介绍了这项工作的前景。2使用JML作为规范语言2.1一个小例子我们使用一个简单的缓冲器系统作为运行示例。 该系统由三个部分组成。每个缓冲器由一个整数值建模,该整数值表示其中的元素数量。系统状态由三个变量b1,B2和B3。系统的最大尺寸为40个元素。系统必须在缓冲器之间分配元素,使得:缓冲器b1小于或等于b2小于或等于b3。 b1和b3之间的差异不应超过15个元素。这些约束在组件之间共享的方式上留下了一些自由。例如,可以存储30个元素,其中b1=5 b2=10 b3=15或b1=8b2=10 b3=12。提出了三种改进方法。初始化将所有缓冲器重置为零。Add(x)通过将x个元素添加到buffer中,使系统的元素总数增加x(x>0);这些元素分布在b1、b2和b3中。Remove(x)通过从buffer中删除x个元素,将系统中的元素总数减少x(x>Y. Ledru等人理论计算机科学电子笔记190(2007)73751public classUncategorized {30}public int b1;public int b2;/*@需要 x>=0 x =5 b1+b2+b3+x =40;&&&&public int b3;@ 修饰b1、b2、b3;5@确保b1+b2+b3==\old(b1+b2+b3)+x;/*@public invariantb1+b2+b3 =40 ;@*/35*//*@public invariant0 =b1; @*/public int findDuplicate(int findDuplicate){/*@public invariantb1 =b2; @*/如果((b1+x)= b2)/*@public invariantb2 =b3; @*/{b1=b1+x;}10/*@public invariantb3-b1 =15;@*/其他40如果((b2+x)= b3)/*@需要true;{b2=b2+x;}@ 修饰b1,b2, b3;其他@确保b1==0&& b2==0 b3==0;&&{b3=b3+x;}15*/}public void run(){45b1 =0;/*@需要 x>=0 x =5 x =b1+b2+b3;&&&&b2 =0;@ 修饰b1、b2、b3;b3 =0;@确保b1+b2+b3==\old(b1+b2+b3)-x;20}*/50public int findDuplicate(int findDuplicate){/*@需要true;如果((b3-x)>=b2)@ 修饰b1,b2, b3;{b3=b3-x;}@确保b1==0&& b2==0 b3==0;&&其他25*/如果((b2-x)>=b1)public void run(){55{b2=b2-x;}b1 =0;其他b2 =0;{b1=b1-x;b3 =0;}Fig. 1. Buffer:JML规范和可能的Java实现2.2Java建模语言Java建模语言(Java Modeling Language,JML)[10]是一种注释语言,用于通过表达类及其方法的形式属性和要求来指定Java程序JML的Java语法使Java程序员更容易阅读和编写规范。该语言的核心表达基于Java,具有新的关键字和逻辑结构。我们在图1中给出的buffer示例上说明JML语法。JML规范出现在特殊的Java注释中,在/*@和@*/之间或以//@开头。每个方法的指定都在其接口声明之前。这遵循了Java工具(如JavaDoc)的通常约定,将此类描述性信息放在方法前面JML注释依赖于三种断言:类不变式、前置条件和后置条件。不变量必须在所有可见状态下保持不变。可见状态大致对应于任何方法调用的初始和最终状态[9]。图1第6行中的不变量表示系统的最大大小为40个元素。JML依赖于契约式设计的原则[12],该原则指出,要调用一个方法,系统必须满足方法的前提条件,而作为对应条件,方法必须建立其后置条件。方法在我们的示例中,Initprecondition被设置为true(参见图1,第22行)。Add和Remove(第32和46行)的前提条件是要添加到(分别)去除)系统为正,小于或等于5,并且不会导致缓冲器超过缓冲器(分别under Escherow).后置条件在ensure子句中表达。例如,Add和Remove的后置条件(图1,第34行和第48行)表示正确执行了添加和删除操作。JML用几个关键字扩展了Java语法。\result表示返回76Y. Ledru等人理论计算机科学电子笔记190(2007)73方法的价值它只能在非void方法的ensure子句中使用\old(Expr)(图1,第34和48行)指的是表达式Expr在方法初始状态下的值。“forall”和“exists”表示普遍的和存在的量化器。3JACK证明义务生成器Java Applet Correctness Kit(或JACK)[2]提供了一个环境,用于验证使用JML注释的Java和JavaCard程序。JACK旨在证明给定Java类的属性,这些属性被单独考虑;这些属性被表示为JML断言。它实现了一个完全自动化的最弱前提演算,从带注释的Java源代码中生成证明义务(PO)。每个证明义务都与程序源代码中的路径相关这些证明义务可以使用不同的定理证明器来履行。Jack proof管理器将证明义务发送给不同的证明者,并跟踪已证明和未证明的证明义务。目前,证明义务可以为B方法的证明器(由Clearsy开发),ESTA定理证明器(特别是由ESC/Java使用),Coq证明助手和PVS生成。对于我们在本文中介绍的案例研究,使用了ESTA。JACK由两部分组成:(1)一个转换器,它是一个引理生成器,从用JML注释的Java源代码转换成适当的形式(例如B引理,用于B证明器),(2)一个查看器,它允许开发人员理解生成的引理。基本概念的数学复杂性是隐藏的。JACK提供了一个专用的证明义务查看器,它可以显示与程序中的执行路径相关的证明义务。目标和假设可以用类似Java/JML的符号显示。布泽尔例子图1提供了Buffer规范的错误实现。实际上,Remove方法是不正确的,因为第57行中的语句可能会将bufferb1设置为负值,同时保持元素总数为正值,这是类不变式所禁止的。对于本例,CNAS(版本1.2.0)无法证明8个证明义务。其中一些对应于正确的代码,并要求用户在规范中添加更多元素以帮助证明者。其他的则对应于错误地实行《撤除》,证明者永远不能确立它们。表1说明了每项证明义务以及相应的规范和代码线图2给出了与Remove方法的不变式保存相关的所有证明义务。4测试过程JML规范可以用作测试过程的oracle。 在本节中,我们首先介绍使用JML进行一致性测试的一些原则,然后介绍Y. Ledru等人理论计算机科学电子笔记190(2007)7377方法PO规格线代码行布·布海尔1616-202716-20添加33437、40、43-444637、40、43-445937、40、43-44去除64851、54、57-587651、54、57-588751、54、57-58表1与未经证实的采购订单(一)(b)第(1)款图二、一个证明义务有关的实施图。1TOBIAS工具。4.1JML作为测试OracleJML具有可执行字符。可以使用不变断言以及前置和后置条件作为一致性测试的预言JML规范由jmlc工具翻译成Java,添加到指定程序的代码中,并在执行过程中对其进行检查。78Y. Ledru等人理论计算机科学电子笔记190(2007)73因此,可执行断言在给定操作的执行之前、期间和之后执行。不变量是必须在所有可见状态下保持的属性。可见状态大致对应于任何方法调用的初始和最终状态[9]。当执行操作时,可能发生三种情况Y. Ledru等人理论计算机科学电子笔记190(2007)7379所有检查都成功:操作的行为符合这些输入值和初始状态的规范。测试结果为通过。中间或最终检查失败:这表明操作的行为与其规范之间存在不一致。实施不符合规范,测试结果为“未通过”。 初始检查失败:在这种情况下,执行整个测试不会带来有用的信息,因为它在特定行为之外执行该测试提供了一个不确定的裁决例如,xmax有一个前提条件,要求x为正数。在那里-因此,用负值检验平方根方法会导致不确定性裁决4.2测试用例定义我们将测试用例定义为一系列操作调用。例如,在下文中,测试用例TC 1对缓冲器系统进行了优化,添加了两个元素,并删除了其中一个。TC1:Init(); Add(2);Remove(1)TC2:Init(); Add(-1)TC3:Init(); Add(2);Remove(3)TC4:Init(); Add(3);Remove(2);Remove(1)每个操作调用都可能导致 PASS、 FAIL或 INCONCLUSIVE裁决。一旦出现 FAIL或INCONCLUSIVE判定,我们选择停止测试用例的执行,并将其标记为该判定。完全执行的测试用例会收到PASS裁决。在缓冲器规范的上下文中,测试用例TC 2和TC 3应该产生一个不确定的结论:在TC2中,Add被调用时带有一个不正确的负参数,在TC 3中,人们试图删除比到目前为止添加的更多的东西。如果测试TC1和TC4是针对“正确”实现执行的4.3测试用例生成组合测试执行给定操作和给定状态的选定输入参数值的组合例如,像JML-JUnit [3]这样的工具生成测试用例,其中包含对类构造函数的单个调用,然后是对其中一个方法的单个每个测试用例对应于构造函数的参数和方法的参数TOBIAS是一个基于组合测试的测试生成器[4]。它使组合测试适应于操作调用序列的生成。TOBIAS的输入由测试模式(也称为测试模式)组成,该模式定义了 一组测试用例。模式是一个有界正则表达式,涉及Java方法及其相关的JML规范。TOBIAS将模式展开为一组序列,然后计算模式所有操作的输入参数的所有组合。80Y. Ledru等人理论计算机科学电子笔记190(2007)73模式可以用组来表示,组是将一个方法或一组方法与典型值相关联的结构化组也可能涉及多个操作。假设S2是一个schema:⎧⎨ S2 = BufGr^{1. 3)与BufGr={Ini t()}|x∈{1,2,3,4,5}}{Remov e(y)|y∈{2,3,5}}BufGr是(1+5+3)=9个实例化的集合。 sunix ^{1.. 3}“重复”是指该组重复1至3次。S2解折叠成9+(9*9)+(9*9*9)=819个测试序列。几个案例研究[1,6]表明,TOBIAS通过允许测试工程师从几行模式描述中生成数千个测试用例来提高测试工程师的生产力。TOBIAS包括将这样的测试套件转换为JUnit文件的工具在所有测试序列开始时,自动添加执行constructorBuffer针对错误的buffer实现执行此测试套件(如图1所示)显示失败:17个测试失败,378个成功,424个不确定。所有失败的测试都报告在执行Remove之后检查不变量的第7行时发生错误。这对应于PO #8。JML不允许指出引入错误的特定语句,因为断言仅在操作退出时进行检查5测试覆盖率测量和证明义务在研究的这一点上,我们知道删除操作中存在错误,PO #8是假的。我们能从测试中得到更多的信心,证明剩下的PO是正确的吗?行覆盖报告是否遇到每个可执行语句。 它也被称为语句覆盖,段覆盖[14],C1和基本块覆盖。基本块覆盖率与语句覆盖率相同,不同之处在于测量的代码单元是每个非分支语句序列对于从S2JCoverage [8]生成的819个测试用例,报告100%的Java语句已经执行。因此,至少涵盖了所有操作,并且在退出这些操作时评估了所有JML断言但是,在这一点上,没有什么可以保证每一项证明义务的路径都已被一项检验所涵盖。评估测试用例TCi是否与w.r.t.相关。一个未经证明的POPOk,第一个简单的想法是评估与TCi相关联的行覆盖率,并将其与POk路径的行进行比较。作为第一个近似,如果TCi没有执行与POk相关联的所有代码行,则它不遵循相同的路径,并且TCi然后与对POk如果TCi至少执行了与POk相关联的所有代码行,那么它可能遵循相同的路径。因此TCi可能与增加POkY. Ledru等人理论计算机科学电子笔记190(2007)7381对于Buberger示例,我们执行了819个测试用例,并使用JCoverage分析了它们的行覆盖率。我们将测试用例的行代码覆盖率收集到25个“包”中给定数据包的所有测试用例覆盖相同的行(可能具有不同的值)。所有17个失败的测试都属于数据包#15。仔细观察数据包#14到#17的覆盖范围,可以发现它们共享Buffer构造函数和Add操作的相同覆盖范围。我们还可以注意到,在这4个包中,行57仅在包#15中执行。我们知道这个错误与Remove操作有关;仔细查看覆盖率信息可以发现错误位于第57行。尽管如此,我们主要关注的是增加我们对未经证实的PO的信心。表2告诉我们,所有测试用例均与PO #1和#2相关。500多个测试用例与PO #3、#4和#5相关,400多个测试用例与PO #6、#7和#8相关。由于失败的测试仅与PO #8有关,我们可以增加我们对未经证实的PO的信心,因为每个PO都已经测试了数百次,并且没有发现任何错误。[5]为了更准确,我们应该从表2中排除不确定的测试。我们打算将这一改进纳入我们报告工具的未来版本分组行代码TC数量PO116-20、27-3031,2216-20、27-30、37、40、43-44701,2,3,4,5316-20、27-30、37、40、43-44、51、54、57-58541,2,3,4,5,6,7,8416-20、27-30、37、40、43-44、51-52、58161,2,3,4,5516-20、27-30、37、40-41、43-44301,2,3,4,5616-20、27-30、37-38、44、51、54、57-58201,2,6,7,8716-20、27-30、51、54、57-58301,2,6,7,8816-20、27-30、51、54-55、57-58121,2,6,7,8916-20、37、40、43-4481,21016-20、37、40、43-44、51、54、57-58321,2,3,4,5,6,7,81116-20、37、40、43-44、51、54-55、57-58231,2,3,4,5,6,7,81216-20、37、40、43-44、51-52、54、57-58381,2,3,4,5,6,7,81316-20、37、40、43-44、51-52、58711,2,3,4,51416-20、37、40-41、43-441021,2,3,4,51516-20、37、40-41、43-44、51、54、57-58311,2,3,4,5,6,7,81616-20、37、40-41、43-44、51、54-55、58141,2,3,4,5,6,7,81716-20、37、40-41、43-44、51-52、58181,2,3,4,51816-20、37-38、40、43-44、51、54、57-58761,2,3,4,5,6,7,81916-20、37、40-41、44、51、54-55、57-58121,2,6,7,82016-20、37-38、40-41、43-44351,2,3,4,52116-20、37-38、44、51、54、57-58631,2,6,7,82216-20、37-38、44、51、54-55、57-58121,2,6,7,82316-20、51、54、57-5861,2,6,7,82416-20、51、54-55、57-58231,2,6,7,82516-20、51-52、54-55、57-58101,2,6,7,8TC合计81982Y. Ledru等人理论计算机科学电子笔记190(2007)73表225个数据包,用于819 Buyer示例测试Y. Ledru等人理论计算机科学电子笔记190(2007)73836使用突变的测量测试集质量的另一种方法是评估其故障检测能力。突变分析可用于此目的。变异分析是基于通过应用变异操作符在实现中播种错误,并检查测试集是否识别出该错误[5,11]。变异的程序被称为突变体。如果测试套件发现了一个突变体的错误,那么这个突变体就被杀死了。一组合适的变异算子应该代表经典的编程错误。突变测试背后的想法很简单:如果一个测试套件杀死了这些操作符生成的所有突变体,那么由于它能够找到这些小的突变体,它很可能擅长发现真正的错误。当使用诸如MuJava [11,13]之类的突变程序时,可能会出现两种问题。首先,将大量的变异算子应用于实际大小的程序通常会导致大量的突变体。其次,有些变种人实际上等同于原程序,无法被杀死。为了限制突变体的数量,我们只将突变应用于与未证明的PO相关的路径中所涉及的语句。例如,我们产生了20个对应于未经证实的PO #7的突变体,我们的测试套件100%杀死了它们。有趣的一点是,对同一包进行不同的测试可能会杀死不同的突变体。这意味着这些数据包具有某种多样性。在案例研究的这一点上,我们已经对剩余证明义务的正确性达到了足够的信心,可以回到交互式证明活动。实际上,只有PO #1到#5值得在这个阶段被证明,因为Remove的更正不会影响它们的正确性。当然,没有什么能保证我们的测试套件能够检测到所有类型的细微错误。这就是为什么最终证明活动是明确需要评估程序的正确性。尽管如此,我们的测试活动的好处是,验证工程师不会浪费时间试图证明错误的证明义务,甚至纠正诸如#6或#7的错误,这可能会被删除的纠正所影响。7银行应用案例研究工业案例研究。证明/测试过程的组合进行了实验,由Gemplus(智能卡制造商)提供的工业案例研究。案例研究是一个处理资金转移的银行应用程序[1]。它由Gemplus ResearchLabs生产,并用于JACK的第一次实验。这个案例研究在某种程度上代表了连接到智能卡的Java应用程序应用程序用户(即客户)可以查询他的账户并从一个账户向另一个账户进行一些用户还可以记录一些“传输规则”,以便安排定期传输。这些规则可以是储蓄规则或支出规则。该案例研究实际上是一个已经在84Y. Ledru等人理论计算机科学电子笔记190(2007)73真实世界,用500个字节写的,分布到8个类中。具体说明见JML。大多数先决条件都设置为true。由于应用程序处理金钱,并且由于某些用户可能具有恶意行为,因此应用程序预期具有防御机制。因此,它应该接受任何条目,但如果输入不是标称行为所期望的输入,它应该返回错误消息或引发异常。为了评估我们的方法,我们在程序的正确版本上工作,并在Currency_src类中引入了一个错误。证明过程。在这个例子中,我们使用了JACK和PACK。由于一些未知的原因,我们只能用JACK工具编译8个类中的7个。 表3报告了JACK生成的采购订单总数和自动证明过程后仍未证明的采购订单数量。测试过程。对于每个类,我们只生成一个TOBIAS模式。它们相当简单,如前面案例研究中的S2他们的设计和使用TOBIAS工具展开只花了我们几分钟的时间。每个模式产生48到1024个测试用例。然后我们执行它们,正如预期的那样,失败的测试只与Currency_src相关。测试范围和证明义务。我们根据语句覆盖率将测试分组到数据包中如表3所示,大多数类对应于少量的数据包。这激发了进一步的研究,使用一些路径覆盖工具,而不是语句覆盖,为了有一个更准确的分布测试用例。杀死变种人由于未解决的技术问题,无法对帐户和规则 对于其他类,我们可以注意到,Balances_src和Transfers_src的所有突变体都被杀死。然而,没有突变体被杀死的储蓄规则和消费规则。显然,测试这两个类都不够相关必须定义更有洞察力的测试模式,以便为这些类生成适当的测试套件,并增加对其正确性的信心。8结论和展望本文提出了一种将证明过程与测试活动相结合的方法。其目的是帮助验证工程师决定未经证明的证明义务的正确性。我们的测试过程从一个组合测试阶段开始,在这个阶段,数百个测试用例是用小的设计任务(很少Y. Ledru等人理论计算机科学电子笔记190(2007)7385模式可以生成几千个测试用例)。它们的执行可能会揭示验证代码中的错误,从而指出错误的证明义务。大量成功的测试,以及对测试套件质量的评估,应该会增加对剩余证明义务的信心提出了两种测试集质量评估技术:语句覆盖率与未证明证明义务相关路径的比较,第一种评估技术将测试套件分布到测试的“包”中第二个评估将突变限制在那些命中出现在未证明PO路径中的语句的突变。测试套件质量的评估可以通过从这两种技术中收集的交叉信息来进一步细化。如果不同的试验能杀死不同的突变体,那么在同一个试验包中进行不同的试验会显示出更多的在Java/JML的上下文中的两个案例研究的方法进行了实验我们使用JACK证明环境、TOBIAS测试生成器以及JCoverage和MuJava进行质量评估。我们将未来的工作分为以下四点:语句与路径覆盖。由于JACK基于路径的概念,因此使用路径覆盖而不是语句覆盖是有意义的。除了我们的环境中没有这样的工具之外,我们怀疑这种更详细的分析会减慢测试过程,并且在某些情况下可能会导致过于详细的测试报告。因此,我们认为应将其作为一种选择。自动程序。我们的方法只有在整个测试过程比交互式证明活动更便宜。每个步骤都是自动化的。JACK自动将PO关联到路径。测试可以自动生成感谢组合工具,如TOBIAS。JCoverage自动分析测试执行期间覆盖的行。通过对JCoverage结果进行排序来完成对测试用例的排序。杀死变种人是自动完成的。报告. 在上一节中,我们提到了交叉包信息与突变分数的潜在利益。计算这一信息的工具仍有待开发。应专门设立更多的设施,类采购订单数量#未经证实的采购订单#TC# TC数据包#突变体死亡人数账户82843MuJava异常余额_src114967241010货币_src9216244321712规则179724MuJava异常SavingRule623148250消费规则372048250转账_src1170560102438181账户管理员_srcJACK(版本1.6.7)无法编译此类表3.银行业实例86Y. Ledru等人理论计算机科学电子笔记190(2007)73用户具有关于其测试质量的综合报告(描述测试与覆盖率、突变分析等方面的相关性)。将断言输入证明过程。TOBIAS生成的测试是独立于代码结构或规范设计的。我们期望它们可以为Daikon不变量生成器提供有趣的输入[7]。这将允许通过测试生成的断言来反馈证明过程,从而产生测试活动的第二个好处引用[1] L. du Bousquet,Y.莱德鲁岛莫里角Oriat和J. - L. Lanet基于JML的软件验证案例研究(短文)。在第19届国际IEEE自动化软件工程会议(ASE'04)的会议记录[2] L. Burdy,A.要求,和J. - L. Lanet Java applet正确性:面向开发者的方法。2003年9月在意大利比萨举行的第12届国际财务和审计专题讨论会[3] Y. Cheon和G.T.莱文斯一种简单实用的单元测试方法:JML和JUnit方法。ECOOP2002,LNCS第2474卷,第231施普林格,2002年。[4] D.M. Cohen,S.R. Dalal,J. Parelius和G.C.巴顿将军自动测试生成的组合设计方法。IEEE Software,13(5):83[5] R.A. DeMillo,R.J. Lipton和F.G.赛沃德测试数据选择提示:对程序员的帮助。Computer,11(4):34[6] S.迪皮伊-切萨湖du Bousquet,J. Bouchet,and Y.勒杜ICARE平台融合机制测试。在第12届交互系统设计、规范和验证国际研讨会上,LNCS第3941卷,第102-113页。施普林格,2005年。[7] Michael D.放大图片作者:William G. Griswold和David Notkin。动态发现可能的程序不变量以支持程序演化。IEEE Trans. Software Eng. ,27(2):99-123,2001.[8] JCoverage主页,2005年。 http://www.jcoverage.com/。[9] JML主页,2005年。 http://www.jmlspecs.org的网站。[10] G.T. Leavens , A. L. Baker , and C. 露 比JML : 详 细 设 计 的 符 号 。In H. 基 洛 夫 湾 朗 普 ,和I.Simmonds , 编 者 , Behavioral Specifications of Businesses and Systems , 第 175Kluwer , 1999年。[11]Y.-- S. 妈,J。O Zuutt,和Kwon Y.R. Mujava:一个自动化的类变异系统软件测试。验证与可靠性,15(2):97[12] B.迈耶采用“契约式设计”。Computer,25(10):40[13] MuJava主页,2005年。 http://www.isse.gmu.edu/faculty/ofut/mujava/。[14] 西蒙·恩塔福斯几种结构测试策略的比较。IEEE Trans. Software Eng. ,14(6):868
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- Simulink在电机控制仿真中的应用
- 电子警察:功能、结构与抓拍原理详解
- TESSY 4.1 英文用户手册:Razorcat Development GmbH
- 5V12V直流稳压电源设计及其实现
- 江西建工四建来宾市消防支队高支模施工方案
- 三维建模教程:创建足球模型
- 宏福苑南二区公寓楼施工组织设计
- 福建外运集团信息化建设技术方案:网络与业务平台设计
- 打造理想工作环境:详尽的6S推行指南
- 阿里巴巴数据中台建设与实践
- 欧姆龙CP1H PLC操作手册:SYSMACCP系列详解
- 中国移动统一DPI设备技术规范:LTE数据合成服务器关键功能详解
- 高校竞赛信息管理系统:软件设计与体系详解
- 面向对象设计:准则、启发规则与系统分解
- 程序设计基础与算法解析
- 算法与程序设计基础概览
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功