理论计算机科学电子笔记190（2007）47-59www.elsevier.com/locate/entcs一种基于模型的测试集全局生成算法Anders Hessel1乌普萨拉大学瑞典乌普萨拉保罗·彼得森2计算机科学与电子学系Vüasteras，Sweden摘要基于模型的测试已经被提出作为一种自动验证系统是否符合其规范的技术。 一个流行的方法是使用模型检查器来产生一组测试用例，通过制定测试生成问题作为一个可达性问题。为了指导测试用例的选择，通常使用覆盖标准。覆盖标准可以被看作是一组要覆盖的项目，称为覆盖项目。我们提出了一个上的-的-的算法，生成一个测试套件，覆盖所有可行的覆盖项目。该算法返回一组跟踪，其中包括填充每个项的路径，而不包括冗余路径。可达性算法仅在状态可能增加总覆盖范围时才探索状态。 这个决定是全局的，因为它不仅孤立地考虑每个单独的本地搜索分支，而且考虑所有分支的总覆盖范围。对于更简单的覆盖标准，如边缘覆盖的位置，这意味着每个模型状态永远不会被探索两次。本文提出的算法已在测试生成工具UPPAALCOJER中实现。我们提出了令人鼓舞的结果，从应用该工具的一组实验和工业规模的案例研究。保留字：基于模型的测试，模型检测，测试用例生成1介绍今天，软件行业中的大部分验证工作都是使用各种测试技术来执行的在一致性测试中，检查已实现系统或系统部分的行为 这通常是在受控环境中完成的，在该环境中，系统被执行并被输入激励1 电子邮件：anders. it.uu.se2 电子邮件：paul. mdh.se1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.08.00548A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）47根据测试规范，并检查系统的响应是否符合其规范。为了降低这个过程的成本，软件测试的执行通常是自动化的，而测试套件的生产大多是自动生成测试套件的技术，或者将生成和执行结合起来的技术，正在出现并变得越来越成熟[31，9，28，19]。在本文中，我们研究了基于模型的一致性测试技术，其中测试套件是在实际测试发生之前从模型自动生成的-有时称为在线测试，与在线测试相反[23]。为了指导测试的生成并描述测试应该有多彻底，我们选择了遵循特定覆盖标准的测试在文献[27，6，12]中已经提出了许多覆盖标准，从简单的结构标准到复杂的数据流标准，其特征在于路径属性。许多算法生成测试套件以下一个给定的覆盖率标准也被提出[29，22，18，13]，包括算法产生测试套件最佳的测试用例的数量，在测试套件的总长度，或在总时间所需的执行测试套件。在本文中，我们研究了测试套件生成算法，这些算法受到了SPIN [16]和UPPAAL[24]等模型检查器中使用的可达性分析技术的启发-这是一种与例如，[19 ]第10段。这些算法本质上执行可达性分析，以生成和探索模型的状态空间，以便找到一组遵循给定覆盖标准的路径，这些路径可以被解释为测试套件。为了生成路径，覆盖标准可以被视为一组独立的覆盖任务[11]或覆盖项目[4]。应用可达性分析为所有可达覆盖项生成一组路径。我们回顾了这种技术，并提出了一些修改，以提高分析的效率。本文的主要贡献是一种新的基于可达性分析的测试集生成算法它可以被看作是一个权衡之间的算法的性能，在时间和空间的要求，并生成一个测试套件与合理的特征。其结果是一个算法，在每一步中使用全局信息的状态空间生成到目前为止，以指导进一步的分析，并加快终止。生成的测试套件是合理的，因为每个覆盖项都是通过从初始状态到第一个找到的状态的路径到达的。在状态空间探索期间，算法存储到目前为止满足的覆盖项的一组路径。该信息用于修剪搜索分支，这些分支将无法对总覆盖率做出贡献-这是一种提高算法性能的技术在实验中，我们证明了这一说法，提出了如何在UPPAAL核心工具3中实现的算法，从文献中的一组例子上执行。本文的其余部分组织如下：在第2节中，我们描述了模型3有关UPPAALcoJER工具的更多信息，请参见网页http://www.uppaal.com/CoVer/A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）4749并对基于可达性分析的测试用例生成技术进行了综述。在第三节中，我们描述了一个可达性分析算法的测试用例生成。在第4节中，我们提出了一种新的算法，用于测试用例生成，使用全局信息的状态空间，以确定终止和修剪。在第5节中，我们描述了比较不同技术的实验结果。本文在第6节中得出结论。相关工作：我们的工作主要涉及受模型检查技术启发的测试用例生成方法，包括[5，13，23，19，17，28]。在[28]中，Nielsen和Skou生成了覆盖事件记录自动机的符号状态的测试用例与我们的工作一样，所提出的状态空间探索算法受到模型检查的启发，但工作重点是定时系统，并使用固定的覆盖标准。在[19]中，Hong等人展示了如何在时序逻辑中表达几个基于时序的覆盖标准，以及如何通过模型检查解决测试用例生成问题Hong和Ural [17]继续这项工作，并研究覆盖项如何相互子索，并提出解决问题的方法。这些工作使用现有的CTL模型检查器来解决测试用例生成问题，而我们提出了一个专门的算法，用于测试用例生成。我们的工作也涉及到定向模型检查技术，其中状态空间探索的属性进行检查。在[8]中，作者使用基于位状态散列的迭代搜索细化方法来指导模型检查器生成测试用例。该方法可以看作是一种迭代使用现有模型检查器的Meta算法。因此，实际的模型检查算法并没有针对测试用例生成进行细化。2预赛我们将提出适用于几种基于自动机的模型的测试用例生成的想法和算法，例如有限状态机，扩展有限状态机（EFSM），例如，SDL [20]或时间自动机[1]。在本文中，我们将介绍我们的结果使用的模型进行通信EFSM。2.1模型动作Act上的EFSMF是一个元组，其中L是一组位置， l0∈L是初始位置，V是具有有限值域的变量的有限集合，E是边的集合。边的形式为<$l，g，α，u，lJ <$∈E，其中l∈L是源位置，lJ∈L是目的地位置，g是上的保护（谓词） V，α∈ Act是一个动作，u是一个更新，其形式是将V中的变量赋值给V上的表达式。EFSM的一个状态是一个元组l，σ，其中l∈L，σ是V的一个映射价值观。 初始状态是σ10，σ0σ2，其中σ0是初始映射。过渡50A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）47对于m∈l，σj−α→σlJ，σJ∈nd是一个possible如果m ∈l，g，α，u，lJ∈E其中g满足σ的赋值，根据u更新σ的结果是σJ，α是一个作用.Act上的EFSM通信网络（CEFSM）是由有限组EFSM F1...，Fn。 网络中的一个状态是一个元组，其形式为：σ1，σ1，.。，，其中是Fi的状态。我们假设一个类似于CCS [26]的握手同步功能然后，CEFSM的转换是（i）一个的内部转换EFSM，即，l， σ，... 我... ，τl， σττ~τ 你好 ， 你好，... ，lJ，σJ，. ，l， σif1 1k k nn1 1k kn n（ii）synchrnofEFSMs，即. ，l， σ，... ，，σ，.，k kk k11 kklm，σm ，σn，σn，σn，σn你好 ， 你好，... ，lJ，σJ，. ，lJσJ，. ，ln，σniflk， σ−α→？11 kkm mklJ，σjlJ，σJ，α？α！互补同步k km m行动无论在什么地方，从上下文中可以清楚地看出，我们将使用表示为s的术语模型状态CEFSM的重新定义以及CEFSM转换的改进的电子束流结构。2.2测试用例生成我们将重点介绍如何生成具有一定覆盖率的测试套件在CEFSM中。测试工程师经常使用覆盖标准来指定测试套件对被测系统的测试程度。在基于模型的测试中使用的覆盖标准的示例包括诸如位置或边缘覆盖的结构标准、诸如定义使用对覆盖的数据流属性、以及关于例如状态的EFSM或时间自动机的时间区域[28，30]。覆盖范围标准通常由要覆盖或达到的项目列表组成。我们将这些项称为覆盖项，并使用C来表示一组覆盖项，C0是初始C，|C|来表示C的大小。如果覆盖标准规定了在例如，数据流标准作为定义-使用对，我们需要处理关于部分满足的覆盖项的信息我们使用定义-使用对覆盖标准[10]来说明这个概念。它应该覆盖所有路径，其中给定的变量x首先在过渡td中的EFSM边ed中定义，然后在过渡tu中的另一个EFSM边eu中使用（通常），而没有沿着从td到tu的路径对x进行任何重新定义。我们将存储这种部分覆盖项，即，x被定义在td中有效的EFSM边ed上，在一个表示为A的集合中。在算法中，我们将CEFSM状态s扩展为（s，C，A）或（s，C），A不需要。我们进一步将模型转换关系扩展到m（s，A，C）∈c（SJ，AJ， CJ），其中R是一个模随机位置s~α sJ，C J和dAJ是根据过渡期达到的覆盖率更新C和As~αSJ. 对于如何更新AJ和Cj的详细描述，例如[14]。我们将使用跟踪来表示从模型生成的测试用例。 我们用的是表示空迹，ω.t表示用变迁t扩展的迹ω。此外，我们使用|ω|以表示ω的长度，定义为|ϵ|= 0w及|ω.t|为|ω|+1。A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）47513一种基于模型检测的测试集生成方法3.1一种局部算法通过可达性分析为给定的覆盖标准生成测试套件的问题已经在文献中的许多设置中进行了研究，参见例如，[25、19、13、4]。本文的作者提出了一种算法，用于从[13]中描述为时间自动机网络的实时系统模型和[4]中描述为扩展有限状态机的非定时系统模型这些算法的一个版本如图1所示，但经过修改，如果算法以广度优先的方式执行，它将返回具有最大覆盖率的最短路径（以步数计）。（01）P ASS：= 0;W AIT：={（s0，C0，N）};ωmax：= 0;max：= 0|了C0|(02) whileWAIT/=0(03)select（s，C，ω）fromWAIT; add（s，C，ω）toPASS(04)对于所有（SJ， CJ，ω. t）：（s，C，ω）<$tc（sJ， C J，ω. t）做(05)如果|CJ|>max(06)ωmax：= ω.t;max：= |CJ|(07)如果<$i（si，Ci，ωi）：（si，Ci，ωi）∈Pass<$WAIT<$si=sJ<$CJ=Ci则(08)add（sJ，CJ，ω.t）toWAIT(09)od(10) od(11) 返回ωmax图1.一种测试用例集生成的可达性分析算法。该算法本质上是一个普通的可达性分析算法，它使用两个数据结构W_AIT和P_ASS来分别保存等待检查的状态和已经检查的状态。此外，全局整数变量max用于（不变地）存储到目前为止见证的最大覆盖率，变量ωmax存储到达具有最大覆盖率的状态的路径。初始PASS为空，而WAIT保持形式（s0，C0，）的初始组合状态，其中s0是模型的初始状态，C0是s0的覆盖，是空路径。重复行（03）至（08），直到WAIT为空。或者，如果预先知道覆盖项的最大数量，则循环可以在达到覆盖在行（03）处，从WAIT获取状态，并且在行（04）处，(04) 生成状态的后继者。在行（05）和（06）处，如果当前后继者覆盖比先前最大值更多的项目，则保存新的路径并且保存新的最大覆盖后继状态（SJ，CJ，ω.t）放在WAIT上52A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）47如果不存在具有相同模型状态和相同覆盖项集合的状态在WAIT和PASS中都找不到si=SJ和Ci=CJ的态（si，Ci，ωi）.它可以被示出（例如，参见，[13，4]），如果行（03）中的选择完成，则图1的算法返回具有最大覆盖的最短路径，使得算法以广度优先顺序探索状态空间重置：注意，图1的算法可能返回不包括所有可行覆盖项的迹ωmax如果模型的状态空间中有两个状态si和sj，使得si不能到达sj，或者相反，则会发生这种情况。我们可以通过在第（04）行为每个后继集添加一个状态（s0，C，ω.reset）来避免这个问题，其中reset是一个不同的符号，表示模型从其初始状态重新开始。这保证了图1中的算法总是返回一条具有所有可行覆盖的路径。覆盖范围包含：在[14]中描述的并且与[7]中描述的包含抽象类似的算法的第一改进是改变行（07），使得使用覆盖项的包含而不是要求覆盖项Ci=CI的相等，即，CJCi.如果存在具有相同模型状态和其覆盖范围的（非严格）超集还可以进一步改进对偶情况下的算法，即，如果一个状态（SJ，CJ，ωJ）放在WAIT上，使得状态（si，Ci，ωi）存在于WAIT或PASS中，其中SJ=si且Cj<$Ci。在这种情况下，可以从WAIT和PASS中移除所有状态（si，Ci，ωi）。请注意，作为结果，一些状态将永远不会被进一步探索。相反，将探索包含状态 这反过来可能会改变搜索状态的顺序。同样的技术已经成功地用于加速模型检查工具，如UPPAAL[2]。其结果是一个算法，探索更少的状态，但普通的广度优先搜索不再保证产生最短的轨迹。3.2部分覆盖图1中的算法适用于覆盖项（即，标准），其可以在单个模型转换中本地确定，诸如位置或边缘覆盖标准。如果覆盖标准规定了一种路径属性，例如在数据流标准中使用的路径属性作为定义-使用对，则必须调整算法以处理关于部分覆盖项的信息。受模型检查启发的用于这类覆盖标准的算法已经在例如，[13、14、4、19]。修改图1的算法相当于将部分覆盖项与普通覆盖项一起存储在结构C中，并修改操作者的行为|C|（第06行）所以A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）4753我 我不考虑部分覆盖项目。也就是说，部分覆盖率以与普通覆盖率相同的方式表示和存储，但在计算（完全满足）覆盖率项目的数量时不考虑它们我们还注意到，上面讨论的覆盖包容并不受C中部分覆盖项的存在的限制。还必须对部分覆盖项目进行重置，即，（s0，A0，C，ω.reset）在后继生成时被添加。4一种全局的测试集生成算法类似于前一节中描述的算法的一个众所周知的问题是探索状态空间所消耗的时间，以及表示WAIT和PASS所需的空间。图1中的算法探索形式为（s，C，ω）的状态，导致状态空间的大小由模型状态s的数量与可能覆盖集C的数量乘积定义（迹ω不影响状态空间中的状态数量）。在本节中，我们描述了避免探索形式（s，C，ω）的所有状态并且仍然生成合理的测试套件的算法。其思想是从整个生成的状态空间中收集和组合信息，以便每个模型状态s不被比必要的更频繁地探索特别地，我们存储一个集合COV，到目前为止所涵盖的所有不同的覆盖项目，即， COV=C 对于所有已探索的状态，（si，Ci，ωi）。额外的信息，包括每个覆盖项c∈COV的跟踪，存储在一个结构SUITE中，用于生成算法返回的测试套件。我们首先在4.1节中描述了一个没有部分覆盖项的覆盖标准的算法，然后在4.2节中描述了一个处理部分覆盖的算法。（01）PASS：=0;WAIT：={（s0，C0，N）};SUITE：=0;COV：=C0(02) whileWAIT/=0(03)select（s，C，ω）fromWAIT; add（s，C，ω）toPASS(04)对于所有（SJ， CJ，ω. t）：（s，C，ω）<$tc（sJ， C J，ω. t）做(05)如果CJ/C，则(06)将（ω.t，CJ）加到SUITE;COV：=COV<$CJ(07)如果<$i（si，Ci，ωi）：（si，Ci，ωi）∈Pass<$WAIT<$si=sJ则(08)add（sJ，CJ，ω.t）toWAIT(09)od(10)（11）returnSUITE图2.一种全局覆盖的测试用例集生成算法54A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）474.1一个全局算法图2所示的算法是图1中算法的修改版本。它以类似的方式工作，但是从所有探索的状态收集覆盖（即，分支）中的变量COV和SUITE。 变量COV包含覆盖率的总集合通过算法找到的项，即， C OV= C 对于所有探索的状态（s，C，ω）。我我我 我对于具有新覆盖的每个探索状态，将元组（ωi，Ci）添加到集合好的这使得S将具有一个迹ω的一组元组匹配到COV中的每个覆盖项。使用普通的广度优先搜索策略，SUITE将以最少数量的模型转换保持对覆盖项的跟踪。在本节的后面部分，存储在SUITE图2中的算法的循环与图1中的算法有两个不同之处。在行（05）和（06）中，如果所探索的状态包含算法之前未见过的新覆盖项，则更新变量C〇 V和S_UITE。注意，在第（07）行中，我们不考虑生成状态的覆盖率CJ因此，状态（sJ，CJ，ω.t）不被进一步探索（即，如果先前已经探索过模型状态sj，则将其添加到WAIT当W_AIT为空时，算法终止，这是当已经探索了来自s0的所有可达状态时的情况。在这一点上，每个模型状态仅被探索一次，COV包含所有可到达的覆盖项，并且SUITE包括到COV中的每个覆盖项的至少一个跟踪。我们将在4.3节中回到从COV生成测试集的问题。4.2部分覆盖我们现在描述如何修改上述算法，以便它可以用于需要部分覆盖项的覆盖标准（类似于第3.2节中提出的修改后的算法）。回想一下，当覆盖标准要求覆盖路径属性时，就需要部分覆盖项，比如定义-使用对标准（见2.2节）。修改后的算法如图3所示。它对形式为（s，A，C，ω）的扩展状态进行操作，其中C和A分别是在到达s的路径ω上收集的覆盖项和部分覆盖项。与图2的算法相比，唯一的主要区别是在线（07）上，其中检查最近生成的状态（sJ，AJ，CJ，ω.t）。这里，如果在PASS或WAIT中存在已经探索的状态（si，Ai，Ci，ωi），其中si=sJ并且AJ<$Ai，则不进一步探索该状态。如果是这种情况，则可以推断出不需要进一步探索（sJ，AJ，CJ，ω i），因为状态不能贡献除了进一步探索（si，Ai，Ci，ωi）将产生的覆盖项之外的覆盖当W为空时，图3 此时，所有已经探索了从s0开始的可达模型状态，COV包含所有可达的覆盖项，并且SUITE是形式为（ωi，Ci）的对的集合，其中ωi是迹结束于覆盖范围为Ci的状态，以及iCi= C OVER. 很容易证明，算法是合理的。它也是完备的，因为对于每个可达的部分覆盖，项ai是扩张态（s，A，C，ω），使得ai∈A.这A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）4755（01）PASS：=0;WAIT：={（s0，A0，C0，N）};SUITE：=0;COV：=C0(02) whileWAIT/=0(03)从W中选择（s，A，C，ω）;将（s，A，C，ω）加到P中(04)对于所有（sJ，AJ， C J，ω. t）：（s，A，C，ω）<$tc（sJ，AJ， C J，ω.t）做(05)如果CJ/C，则(06)将（ω.t，CJ）加到SUITE;COV：=COV<$CJ(07)如果<$i（si，Ai，Ci，ωi）：（si，Ai，Ci，ωi）∈PASS<$WAIT<$si=sJ<$AJ<$Ai(08)然后将（sJ，AJ，CJ，ω.t）加到WAIT(09)od(10)（11）returnSUITE图3.一个具有部分覆盖项的全局算法保证所有可行覆盖项都将生成，因为项ci∈COV仅依赖于A中的一个（或零个）部分覆盖项。4.3改进测试套件当上述算法终止时，S_UITE是集合{（ω0，C0），.，（ωn−1，Cn−1）}.理想情况下，应减少此集合，以便总覆盖率ΣiCi不变，以及测试套件的长度，即，我|ωi|，被最小化。剩余的迹线ωi然后可以用作测试套件。然而，选择具有此属性的迹的子集是众所周知的集合覆盖问题的一个版本，这是NP难的[21]。同样众所周知的前缀消除技术可以用作问题的近似解决方案，即，为了确保在SUITE中没有迹对ω，ωJ使得ω是ωJ的另一个前缀。然而，这种方法有一些明显的问题，包括SUITE仍然可能包括冗余迹线的事实，即可以在不减少SUITE的总覆盖率的情况下移除的迹线。我们已经选择了一个算法，可以增量执行，作为主要的测试用例生成算法的一部分当主算法终止时，它也可以应用于SUITE 它检查S中的每个（ωj，Cj）满足条件Cj<$C0<$. Cj−1 n−1，即， （ωj，Cj）对SUITE的总覆盖率有贡献。正如我们将在下一节中看到的，这种方法在我们的实验中效果很好。56A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）47表1算法的时间（以秒为单位）和空间（以MB为单位）性能局部算法时间序列状态树全局算法时间序列状态树充分火车e 6（0）复位2.9 9.6 15 3353 13.85 10.5 15 7375 11.25 9.3 15 1645 1- -充分火车du 12（5）复位37 14 47 27129 1107 33 47 114697 12.4 9.3 l56 1717 4- -止动件30飞利浦du 109（42） 停止60充分9 10 30 5797 11085 87.7 69 461305 1- -1 9.2 80 170 8204 393 1616.4 10.6 681 7579 37止动件20止动件30WAP e 68（0）停止部件68充分4.29 12.7 55 5105 130.8 31.2 86 35615 1- （7348332）0- -4.17 12.5 161 4361 54.51 12.5 175 4395 538 32 818 37503 123871 1946 818 3850877 12止动件20止动件30WAP ei 68（68）停止部件68充分10.85 12.7 58 5404 1525 52 93 71328 1- -- -8 12 58 5299 115.9 14.9 189 7291280 111.2 1718 200011 194093 2025 1718 3937243 195实验对于本节中的实验，我们使用我们的工具UPPAALcoCER，它将时间自动机模型和覆盖标准作为输入。型号和覆盖标准：我们将使用文献中记录的三个模型：一个火车门示例（Train），其中模拟了四辆火车和一个控制器[32]，Philips（Philips）[3]的带有总线冲突检测的音频控制协议，以及[15]中建模和测试的WAP堆栈（WAP）。我们提出了三个不同的覆盖标准边缘（e），定义-使用对（du）和边缘初始化（ei）的实验。在边覆盖准则中，覆盖项是自动机中的遍历边。如果使用同一个自动机的多个实例，它不会区分行使边的不同实例。du-pair准则在本文的第2.2边缘初始覆盖准则要求执行边缘，如在边缘覆盖准则中那样。为了满足覆盖项，测试用例还必须将系统恢复到与初始系统状态相似的状态。结果如下：在表1中给出了局部和全局算法的性能。 在SUN Ultra SPARC-II 450 MHz上使用广度优先搜索策略执行算法。表格最左边的一列指定了实验中使用的输入，即，模型、覆盖标准、覆盖项目的数量，以及（括号中）模型中存在的部分覆盖项目的数量。在第二列中，使用以下关键字：full用于穷举搜索，stop x用于在找到x个覆盖项后终止，如果在模型中使用重置，则重置（如第3.1节所述，这仅适用于局部算法）。对于当地和A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）4757全局算法我们给出以下数字/列、生成时间（time）、存储器（RAM）、轨迹长度（len）、生成的状态数（states）和生成的轨迹数（tr）。标记为Train e 6（0）的行显示了列车自动机实例上具有边缘覆盖标准的列车门模型的性能。有六个覆盖项目需要覆盖，零个部分覆盖项目。全局算法生成1645个状态，这是模型的大小。本地算法分别产生3353或7375个不带复位和带复位的状态。对于Train du 12（5）行，使用了定义-使用标准。有12个不同的覆盖标准和5个部分覆盖项目。全局算法生成的状态空间的大小适度增加（由于部分覆盖项）到1717（+4。3%，与模型状态空间的实际大小相比）。对于局部算法，这种增加是从3357个状态增加到27129个（或者当使用复位时增加到114697个我们注意到，全局算法的性能大大优于局部算法。事实上，它只生成本地算法所使用的状态的6%（或2%）。执行时间的增加是类似的。对于表中其余部分的模型，我们无法使用局部算法进行详尽分析，也无法使用重置。实验结果还显示了算法如何针对不同的模型和覆盖标准进行扩展在所有的例子中，全局算法优于局部算法。6结论在本文中，我们已经研究了算法和思想的测试套件生成applicable自动机模型的语义定义为（有限）转换系统。我们已经审查了来自普通的可达性分析算法，类似于那些在许多模型检查和规划工具。这样的算法可以用来生成遵循给定覆盖标准的测试套件，并且在例如测试套件将执行的模型转换的总数方面是最优的。 我们进一步阐述了这些算法，采用现有的抽象和修剪技术经常使用的模型检查算法。本文的主要贡献，是一种新的全球算法基于模型的生成测试套件以下一个给定的覆盖标准。在任何给定的点，该算法-其灵感来自于先前描述的可达性分析算法-使用关于在当前生成的状态空间中发现的总覆盖的知识来指导和修剪剩余的探索。这样，算法避免了不必要的探索，并生成具有合理特征的测试集本文提出的所有算法已在我们的测试用例生成工具UPPAALcoCER中实现。为了比较和评估的算法，我们已经进行了大量的实验，一组模型先前在文献中描述的。特别是，评估给出的实验证据表明，所建议的全局算法使用的内存和时间大大少于本地al-出租，并输出测试套件，是不远处的最佳。在这方面，58A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）47所建议的全局算法增加了模型的最大大小，可以针对该模型通过算法生成测试引用[1] R. Alzheimer和D. L.迪尔时间自动机理论。Theoretical Computer Science，126（2）：183-235，1994.[2] G. Behrmann，J. Bengtsson，A. David，K. G. Larsen，P. Pettersson，and W.逸乌帕尔实施的秘密。在FTRTFT史普林格出版社[3] J. Bengtsson，W.O.David Gri Bogoen，K.J. Kristo Pastersen，K.G. Larsen，F.Larsson，P.彼得森，以及W. 逸使用UPPAAL验证具有总线冲突的音频协议。In R.Alzheimer和T.A.Henzinger，editors，Proc. 第八届国际Conf. 关于计算机辅助验证，计算机科学讲义第1102卷，第244-256页。Springer–Verlag, July[4] J. Blom，A.埃塞尔湾Jonsson，和P.彼得森基于Observer的测试用例生成自动机Gabowski和B. Nielsen，编辑，Proc.4thInternational Workshop on Formal Approaches to Testingof Software 2004（FATESSpringer–Verlag,[5] R. 卡德尔-奥利弗用时间自动机进行实时系统的一致性测试Formal Aspects of Computing，12（5）：350[6] L. A. Clarke，A. Podgurski，D. J. Richardsson和Steven J. Zeil。数据流路径选择标准的正式评估。IEEE Trans. 软件工程，SE-15（11）：1318 -1332，1989年11月。[7] 孔拉多·道斯和斯塔夫罗斯·崔帕基斯使用抽象的实时可达性属性的模型检验。在Bernard Ste Escheren，编辑 ， Proc. of the4thWorkshop on Tools and Algorithms for the Construction and Analysis ofSystems，number 1384 in Lecture Notes in Computer Science，pages 313-329. Springer–Verlag,[8] J.P. Ernits，A. Kull，K. Raiend和J. Vain。使用引导模型检查和迭代搜索细化从efsm模型生成测试。在K。Havelund，M. Nez，G. Rosu和B. Wol Wei，编辑，FATES/RV 2006，计算机科学讲义第4262卷，第40-54页。Springer-Verlag，2006.[9] J.- C. Fernandde z，C. Jard，T. J'eron，和DC。 万岁。对采用验证技术的协议的自动生成单元进行优化。计算机程序设计科学，29，1997。[10] P. G. Frankl和E. J. Weyuker.适用的数据系列符合测试标准。IEEE Trans. Softw. Eng. ，14（10）：1483[11]G.弗里德曼，A. Hartman，K. Nagin和T.希兰用于软件测试的预计状态机覆盖率。在Proc. ACM SIGSOFT软件测试和分析国际研讨会上，第134-143页[12] 下午赫尔曼程序测试的数据流分析方法 澳大利亚计算机杂志，8（3），1976.[13] A. Hessel，K.G. 拉森湾Nielsen，P.Pettersson和A.Skou. 时间最优的实时测试用例使 用 UPPAAL 生 成 。 以 . Petrenko 和 A.Ulrich ， 编 辑 ， Proc.3rdInternational Workshop on FormalApproaches to Testing of Software 2003（FATESSpringer–Verlag,[14] A. Hessel和P.彼得森实时系统的测试生成算法在H-D。埃里希和K-D Schewe，编辑，第四届国际软件质量会议论文集，第268-273页。IEEE计算机协会出版社，2004年9月。[15] A. Hessel和P. Pettersson。WAP网关的基于模型的测试：行业研究。在洛帽檐和M.第11届工业关键系统形式化方法国际研讨会论文集（FMICSSpringer–Verlag,[16] G.J. Holzmann模型检查器SPIN。IEEE软件工程学报，SE-23（5）：279[17] H. S. Hong和S.乌拉尔使用模型检测降低测试生成的成本 在j.加博夫斯基和B.Nielsen，editors，Proc. 2004年第四届软件测试形式化方法国际研讨会（FATES'04），计算机科学讲义第3395卷，第110-124页。A. Hessel，P.Pettersson/Electronic Notes in Theoretical Computer Science 190（2007）4759[18] H.S. Hong，S.D.查岛李湾，澳-地Sokolsky和H.乌拉尔 数据流测试作为模型检查。 在ICSE'03中：第25届国际Conf. 2003年5月，第232-242页。[19] H.S.洪岛李湾，澳-地Sokolsky和H.乌拉尔基于时序逻辑的测试覆盖理论。在J. - P. Katoen和P. Stevens，编辑，系统构建和分析的工具和算法：第8届国际会议，（TACASSpringer–Verlag,[20] 国际电联，日内瓦。ITU-T，Z.100，Specification and Description Language（SDL），1999年11月[21] R. M. 卡普组合问题中的约简。在托马斯·J编辑，计算机计算的复杂性，Proc.Sympos。，第85-103页。IBM，1972年。[22] M. Krichen和S.Tripakis。实时系统的黑盒一致性测试 在Laurent MounierSusanneGraf，编辑，Proc. 第11届国际SPIN模型检测软件研讨会（SPIN'04），计算机科学讲义第2989卷，第182-197页。[23] K. G. 拉森，M。 Mikucionis，和B. 尼尔森 使用uppaal进行实时系统的在线测试。在Gabowski 和 B. Nielsen ， 编 辑 ， Proc.4thInternational Workshop on Formal Approaches to Testing ofSoftware 2004（FATESSpringer–Verlag,[24] K. G. Larsen，P.Pettersson和W.逸你在坚果壳里。 软件工具国际技术转让，1（1[25] D. Lee和M.扬纳卡基斯通信协议特性测试中的优化问题。icnp，00：66，1996。[26] R.米尔纳 通信和并发。 Prentice Hall，Englewood Cli，1989.[27] G.迈尔斯 软件测试的艺术。 Wiley-Interscience，1979年。[28] 布莱恩·尼尔森和阿恩·斯库。从时间自动机自动生成测试。International Journal on Software Tools forTechnology Transfer，5：59[29] S. Rapps和E. J. Weyuker.利用数据流信息选择软件测试数据。IEEE Trans. Softw. Eng. ，11（4）：367[30] J. Springintveld，F.Vaandrager和P.R. 测试时间自动机。Theoretical Computer Science，254（1-2）：225[31] J. Tretmans和A.贝琳凡特使用形式化方法进行自动测试。1999年11月8日至12日在西班牙巴塞罗那举行的第七届欧洲软件测试国际会议上&欧洲之星会议，戈尔韦，爱尔兰。[32] W. Yi，P.Pettersson，and M.丹尼尔实时通信系统的自动验证通过约束求解。在Dieter Hogrefe和Stefan Leue编辑的第七届形式描述技术国际会议论文集（FORTENorth–Holland,
