基于数据抽象的测试用例自动生成技术在软件测试中的应用

理论计算机科学电子笔记191（2007）25-48www.elsevier.com/locate/entcs基于数据抽象的参数化测试用例自动生成延斯河Calam'e1NataliaIoustinova2JacovandePol3部of Software Engineering Centrumvoor Wiskunde en Informatica荷兰阿姆斯特丹摘要开发测试套件是一个代价高昂且容易出错的过程。基于模型的测试生成工具通过从系统模型自动生成测试用例来促进这一过程。然而，这些工具的适用性取决于目标系统的规模在这里，我们提出了一种方法来生成测试用例相结合的数据抽象，枚举测试生成和约束求解。给定一个可能无限系统的具体规范，数据抽象允许导出一个抽象系统，它是有限的，因此适合于使用枚举工具自动生成抽象测试用例。 为了执行抽象的测试用例，我们必须实例化它们具体的数据。对于数据选择，我们利用约束求解技术。关键词：一致性测试，基于模型的测试，测试用例生成，数据抽象，约束求解。1介绍软件故障可能会带来昂贵或危险的后果，因此确保软件产品的质量非常重要。软件测试作为一种验证软件产品的动态方法，已被学术界和工业界广泛接受。根据对被测实现（IUT）的看法，可以区分白盒测试和黑盒测试。虽然有关于IUT的内部细节的知识可用于白盒测试，但在黑盒测试中测试过程包括测试套件的设计、实现和执行。这些阶段中的每一个对于复杂的1电子邮件：jens. cwi.nl2电子邮件：natalia. cwi.nl3电子邮件：vdpol@cwi.nl1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.01926J.R. Calamé等人/理论计算机科学电子笔记191（2007）25系统规范（例如：UML）数据抽象TTCN-3一代约束生成测试生成器测试目的系统规范（正式）数据选择可参数化测试用例（例如TTCN-3）抽象测试用例抽象系统规范Fig. 1. 测试生成过程真实的系统因此，正在进行研究以自动化这些阶段中的每一个。在本文中，我们提供了一种方法，自动生成基于模型的测试黑盒测试。测试用例可以从测试模型（即测试套件的模型）或IUT的模型中生成。在第一种情况下，测试用例与IUT的模型分开设计，例如使用UML 2 Testing Profile[27]等框架。这导致了很好的测试用例，但也可能在开发过程中加倍建模工作量。在第二种情况下，IUT的现有模型由测试用例生成器检查。基于模型的测试生成是针对一致性测试而开发的，其目的是检查IUT是否符合其规范[22，33]。现有的基于模型的测试生成器通常依赖于规格的状态空间的枚举。对于由多个组件组成的开放系统，相互通信以及系统环境，枚举方法导致大量（有时是无限）的测试用例。在这里，我们提出了一种结合数据抽象、枚举测试生成和约束求解的方法来解决这个问题（见图1）。给定一个开放系统的规范，我们应用已经成功应用于模型检查开放系统的数据抽象（例如[30]）。得到一个（有限的）抽象系统。 从抽象的系统，我们生成一组抽象的测试用例。这些测试用例的生成是由测试目的[22]指导的，它定义了感兴趣的场景。生成的抽象测试用例包含抽象数据，这些数据应该在测试执行之前具体化为了用具体的数据实例化抽象的测试用例，我们采用了约束求解.在测试生成和抽象的同时，我们将原始规范转换为规则系统，进一步用于数据选择。为了检索测试数据，将测试套件转换为测试预言机。我们使用这些数据来实例化测试用例并执行它，在执行过程中，IUT可能会偏离选定的路径。通过在线约束求解，我们动态地适应测试执行的过程本文的组织如下：在下面的小节中，我们讨论了与我们的测试生成方法相关 在第2节中，我们给出了一个概述J.R. Calamé等人/理论计算机科学电子笔记191（2007）2527一致性测试。在第3节中，我们描述了我们正在使用的规范的语法和语义。 第4节中给出了约束求解的方法。 在第5节中，我们描述了我们的数据抽象方法， 第6节中测试生成的解释。 我们将我们的方法应用于案例研究，这在第7节中描述。 最后，我们以第8节结束。 本文引理的充分证明可以在[4]中找到相关工作最接近我们的方法是符号测试生成[8，14，23，29，36]。这种方法直接适用于作为输入输出符号转换系统给出的更高级别的规范，而无需枚举它们的状态空间。 给定测试目的和规格，他们的产品就构建好了。这些作品是建立在ioco理论[32]。在这些情况下，抽象解释[10]过度近似了可达性分析。使用验证技术（TGV，[22]）生成测试的概念也基于ioco。在我们的方法中，抽象技术的目的和使用在概念上与符号测试生成不同，因为我们使用数据抽象来避免外部数据引起的不确定性。这使我们能够使用现有的枚举测试生成技术来获得抽象的测试用例，这些测试用例是通过约束求解得到的具体数据来实例化的。在符号测试生成方法中，使用近似可达性分析来修剪可能不会导致通过判决的路径。这两种方法都适用于任何导致IUT他们都采用约束求解选择一个单一的测试策略在测试执行。哪种方法实际上更适合哪类系统，只能通过广泛使用方法。白盒测试的测试数据确定[17]已在最近的几篇论文[16，31，34]中进行了讨论。它们主要基于符号执行技术[9，24]。我们生成的用于确定测试数据的约束规则系统与[28]相当，其中还生成了对可见输入和输出、保护和内部状态变化进行编码的约束规则。 这些规则用于通过将整个系统规范转换为Prolog来生成一组测试用例。然而，测试用例已经存在于我们的案例中，规则系统只需要找到具体的测试数据。2测试理论我们的方法基于一致性测试，该测试验证实现是否符合其规范。在一致性测试的理论中，一致性的概念是通过规范和实现之间的一致性关系来形式化的，这些规范和实现被假设为输入输出标记转换系统（IOLTS）。 在本文中，我们参考了[22]中描述的理论的一个变体。这里不讨论静止IOLTS是具有非空状态集的元组（，Lab，→，σinit），28J.R. Calamé等人/理论计算机科学电子笔记191（2007）25⊆--→→→⊆ ×××→init→专用的初始状态σinit、动作标签Lab的字母表和转换关系Σ Labε。标签Lab的集合由三个动作子集组成，LabI，LabO， τ表示输入、输出和内部动作。输入和输出操作是可见的，内部操作是不可见的。IOLTS是确定性的，如果在每个状态中对于每个动作λ∈Lab最多存在一个传出转移，σ∈Σ。IOLTSM的行为由状态和跃迁序列β=σinitσ1给出... 从初始状态开始。 轨迹是通过投影其中，[M]是一组IOLTS M的迹线。之后的关系被定义为状态集<$J，如果系统处于状态σ并且执行动作λ，则可以达到该状态集（<$J=λ之后的σ）。它也被定义为可能在执行跟踪β之后启用的动作λ（λ之后的J= β）。IOLTS的建模IUTs被假定为输入完整的，即实现不能拒绝来自环境的任何输入。给定一个实现的模型MIUT和一个规范的模型MSpec，该实现符合[MSpec]]跟踪中每个跟踪β的规范，该跟踪β之后的MIUT只产生β之后的MSpec可以产生的输出。如果MSpec是输入完成的，则一致性是标准跟踪包含关系4。我们对测试生成感兴趣，其中测试选择由测试目的指导[22]。测试目的是一个确定性的IOLTSMTP，它配备了一组非空的接受状态Accept和一组可以为空的拒绝状态Refuse接受状态和拒绝状态都是陷阱状态，即任何行动都不能再离开他们此外，除了接受和拒绝状态外，所有状态下的MTP都是完全的这意味着在所有状态下，MSpec中可能的所有操作都被启用。假设1（测试目的中的数据处理）我们 假设 的 测试目的MTP仅关注所述场景的控制流程，因此LabTP的标签中携带的动作信息仅限于动作名称。数据参数不应该是赋值的对象，因此被不关心的参数所取代。由测试目的引导的测试生成包括用MTP构建M Spec的标准同步产品M SP，并通过将判决指定为测试用例实例的可能结果，最终将其转换为完整的测试图M CTG（参见定义2.2）。同步乘积MSP的状态空间构成了同步规范RTP的可达部分。 集合SP是通过匹配M Spec和M TP的转换来构造的。接受状态的集合被定义为acc={（s，ACCEPT）|s ∈Spec}。定 义 2.1 （ 完 全 测 试 图 [22] ） 完 全 测 试 图 CTG 是 IOLTSMCTG= （ ΣCTG ，LabCTG，CTG，σCTG），其以以下方式从合成乘积MSP(i) 通过镜像MCTG的动作集合来确定动作集合：[4]与ioco[32]的不同之处在于，我们没有从τ-步骤中抽象出来，而且我们还没有考虑静止。J.R. Calamé等人/理论计算机科学电子笔记191（2007）2529L2a失败O我→ACC∈\⎪∈∧||没有，我|β| =零⎨⎧我⎪OO我我O通过L2aL2aβACC失败失败失败L2aL2aL2a因康茨L2a我因康茨失败失败L2a我Lab CTG= Lab CTGLab CTGwith Lab CTGLab Specand Lab CTG= Lab Spec.(ii) 状态集被划分为四个子集：及CTG及CTG，其定义如下：L2a因康茨失败要接受的销售线索：CTG ={σ ∈SP |<$β ∈ [[MSP]]迹（σ →SP σJ <$ΣJ∈<$SP）}，通过：集合CTG CTG被定义为CTG = SP。 这一套可能不会为空.通过L2a通过ACC不确定性：={σJ| <$σ∈<$CTG，σJ/∈<$CTG，λ∈Lab SP（σ →λσJ∈→SP）}，因康茨L2aL2AO未通过：CTG={σ CTG}，σ CTG/∈SP（隐式状态）。(iii) CTG的转换集 定义为→CTG =→CTGCTG因康茨TCG →CTG，其中：• →CTG=→SP（CTG×LabCTG×CTG），• →CTG=→SP（CTG×LabCTG×CTG），• →CTG ={σ →λσ CTG|σ ∈ <$CTG <$λ ∈ LabCTG<$σ after λ =<$}。在CTG中镜像输入和输出的原因在于测试用例和IUT之间的关系，因为IUT的输入是测试用例的输出，反之亦然。然而，由于测试用例通常不能测试所有可能的IUT的输入，其输出集LabCTG仅限于IUT的子集通过构建MSpec和MTP的同步产品，CTG可以包含相同状态下的几个输出之间或输入和输出之间的循环和选择因此，它是不可控制的，即。测试器例如不能自动决定是否期望来自IUT的输入或向其发送输出MSP的接受和拒绝状态集分别导出接受和拒绝迹集，记为[MSP]] atrace和[MSP]]rtrace。 [M SP]] atrace是以状态σ_SP和[M SP]] rtrace=[[M Spec]] trace[[M SP]] atrace结束的那些迹。根据实际测试期间执行的跟踪，分配一个判定以评估IUT的正确性。定义2.2（声音判定）判定的P re定义值：Pas s、Incon c、Fail和None。判决由函数setverdict：[M SP]] traceVerdict设置，其中：通过，iβ[[MSP]]atraceβ>0setverdict（β）=Inconc，i <$β ∈ [[MSP]] rtrace<$|β|> 0个失败，i <$β/∈ [[M SP]] atrace<$[[M SP]] rtrace<$|β|> 0个通过判定被分配给MCTG的那些状态，这些状态对应于来自[MSP]]atrace的跟踪的最终状态，因此对应于测试目的中的接受 Inconc判定被分配给接受状态不可到达的状态。 在本例中，状态仍在MSpec的跟踪上，但跟踪不满足测试目的（来自[MSP]]rtrace的痕迹）。所有未指定的输出导致∪ →30J.R. Calamé等人/理论计算机科学电子笔记191（2007）25∈→ × ×→→ × × →∈Bool排序funcT：→Bool F：→Boolmap和 ： Bool×Bool→Boolvarb ：Boolrew和（T，b）=b和（b，T）=b和（F，F）=F图二. 布尔型的数据类型失败的判决如前所述，M CTG可以包含几个输出之间的选择以及输入和输出之间的选择。本文所处理的测试用例是无环的和可控的。一个可控的测试用例M TC是通过解决上述选择，即。测试用例不再包含输出之间或输入与输出之间的这些选择。 测试用例与IUT并行执行。选择导致通过状态的迹线β [[M TC]]通过。从该跟踪，具有一个步骤的几个分支导致Inconc状态，其表示以拒绝状态结束的测试目的中的跟踪使用测试目的作为选择标准，可以在不生成规范的整个状态空间的情况下生成测试用例。然而，由于所有可能的数据，一个完整的测试图3规格说明的语义与语义在本节中，我们定义了我们正在使用的系统的语法和语义。规范Spec由五元组Spec=（Sort，Fun，Act，Comm，Proc）给出（规范语言μ CRL见[18]）。它指定了一个与其环境通信的开放系统。Sort定义了一组用于声明变量的数据类型。对于每个排序S，存在一组构造函数，其形式为c：S或c：S1...SnS，对于S1，...，Sn有点。 这些构造函数用于形成排序为S的值。在Fun中，f：S或f：S1形式的函数... Sn S， 已经宣布。这些函数中的每一个都由一个或多个公理定义，这些公理是关于S1，...，Sn.这些公理的形式为s=t，其中s和t是由类型变量和函数符号的任何有效组合形成的等价类型项。图2显示了一个表示布尔值的排序Bool（参见sort），它由两个构造函数T（表示true）和F（表示false，参见func）给出。函数和在映射中被定义为具有定义和的性质的三个公理（见rew）。此外，b被定义为Bool类变量（见var）。动作集Act和通信动作集Comm是声明过程定义所需的动作和通信问题所必需的。然而，我们将不在这里详细讨论它们。 过程本身被定义为线性过程算子的Proc[1]。然而，为了使图形表示成为可能，我们根据符号转换理论给出了过程的定义J.R. Calamé等人/理论计算机科学电子笔记191（2007）2531∈∈ ⊆ ×××{|→}→ → ⊆ ××→→l−→？s（x）<$l∈Edg<$v∈D（l，η）−→？s（v）（n，η[x<$→v]）极输入l −→g<$ ！s（e）l∈Edg [[g]]η=true[[e]]η=v（l，η）−→！s（v）（n，n）l−→g<$x：=e<$l∈Edg[[g]]η=true[[e]]η=v（l，η）→τ（nl，η[x<$→v]）输出信号表1过程定义P（Spec→M）的步骤语义Sition Systems. 因此，过程定义Proc可以用四元组（Var，Loc，σinit，Edg）来描述，其中Var表示变量的有限集合，Loc表示位置或控制状态的有限集合。变量到值的映射称为赋值;我们用Val= ηη：变量D. 设Σ init =Loc Val为状态集，其中进程有一个指定的初始状态σinit=（linit，ηinit）- 是的 关于Edg Loc法Loc表示边的集合。边描述了由一个动作从一组动作指定的配置的变化。将位置视为节点，将边视为边，这样的规范也可以图形化地表示为符号转换系统。作为动作，我们区分（1）具有可以赋值的局部变量的信号s的输入，（2）信号s连同由表达式描述的值的输出，以及（3）赋值。除了输入之外的每个动作都由布尔表达式g保护，g是它的保护。这三类行为被写为？s（x），gD！s（e），和g Dx：= e，我们使用α，αJ.. 当离开这类诉讼时， F或边（l，α，l）∈Edg，我们记为更简单的l−→αl.然后，过程的行为由状态序列给出：σ1... 从最初的一个开始。 步骤语义由IOLTS给出M =（λ，Lab，，σinit），其中，Σ Lab Σ是状态之间的标记转移关系。标签区分内部τ-步骤和通信步骤，输入或输出，这是由一个信号和一个正在传输的值，即标记？s（v）或！s（v），分别。我们假设来自环境的信号集和系统内交换的信号集是不相交的。语义由表1中的推理规则给出。 用通信天线接收信号，l−→？s（x）<$l∈Edg，根据信号的参数（规则I输入），得到η[x <$→ v]的更新值。输出，l −→g<$！s（e）lEdg是受保护的，因此发送消息涉及评估保护和根据当前估值。 它会导致发送消息的进程的位置发生变化（规则输出）。 赋值nts，l−→g<$x：=e<$l∈Edg，导致位置的改变和赋值η[x <$→v]的更新，其中[[e]]η= v。因为它们是内部的，所以赋值转换用τ（规则ASSIGN）标记虽然我们使用的规范只包含一个过程定义，ˆ32J.R. Calamé等人/理论计算机科学电子笔记191（2007）25≤不DD−−PD|−∧ ∧≥美国DTTDD|这并不限制我们的方法。我们的方法的实现适用于线性过程算子[1]。对于这些，现有的线性化技术[19]可以用于通过消除通信和并行组合来获得有限数量过程定义的4约束求解矩阵在本节中，我们将概述与约束求解相关的概念[25]。一个约束域由一组描述关系和逻辑理论的n元约束符号组成。 此类约束符号的示例 是““。原始约束c（X1，...，Xn）是由约束符号和每个参数位置的相应值集合Vi中的项构造的。原始约束的一个例子是≤（X，Y），定义了关系X≤Y。约束的形式为C = c1.其中m0和c1，.，c，m是原始约束。我们使用vars（C）来表示约束C的变量集。 约束C的赋值θ是变量vars（C）到值的映射的V1，...， Vnin.一个逻辑理论决定了在某个赋值θ下哪些约束成立，哪些约束不成立。如果约束C在约束域理论下对赋值θ成立，则记为=[[C]]θ。有两个不同的约束真和假，它们对任何理论都是一样的。重言式的真总是成立的，而矛盾式的假永远不成立。与C相关的两个问题：解决方案问题和满意度问题。第一个确定一个特定的解决方案，后者确定是否有至少一个解决方案。 设θ是C的一个赋值。 θ是一个解若[C]]θ成立，即 =[[C]]θ。一个约束C是可满足的，如果它至少有一个溶液约束域的约束求解器solv（）是一个决策过程，它将约束C作为输入，并返回true、false或unknown。当solv（C）返回true时，C是可满足的。当solv（C）返回false时，C没有解，并且C是不可满足的。 unknown值表示，可能存在解决办法，但无法确定。用户定义的约束的形式为p（t1，.， 其中p是n元谓词，并且t1，...， tn是来自约束域的项 （ 变 量 、 常 数 或 函 数 ） 。 用 户 定 义 约 束 的一个例子是 （ X ， f（Y）），它有两个参数（变量X和函数f（Y），Y也是一个变量）。 字面量是原始约束或用户定义的约束。例如在Prolog中，规则R的形式是A：B，其中A是用户定义的约束，B是文字序列。例 如 ，a（X，f（Y））：X> 0，Y 0和Y 0。 如果m=0，则G是一个空查询，记为Q。令查询G具有以下形式：J.R. Calamé等人/理论计算机科学电子笔记191（2007）2533不→TT→⟨|⟩−×···× → ×···×→L1，...，L（i1），Li，L（i+1），.，Lm和Li=p（s1，...，sn）。 约束逻辑程序中的状态由一对GC给出，其中G是实际目标，C是约束存储，存储此状态的所有相关条件这些状态之间的转换是派生步骤。 求导[25]是从初始状态到最终状态的完整迹，|C1级... 中国|C.5数据抽象在本节中，我们将描述数据抽象的思想，以封闭开放系统来生成测试。 首先，我们解释的方法，在我们讨论之间的关系，一个具体的和抽象的系统。我们不对IUT的环境做任何假设，即我们采用最一般的环境。因此，来自环境的信号可以具有任何值。这通常会将系统的状态空间提升到无穷大。我们将直接或间接受环境影响的数据抽象为单值混沌，表示为。不受环境影响的价值观仍然是原始的价值观，因此应该以与原始系统相同的方式对待它们这种数据抽象在[30]中首次提出，用于模型检查开放系统。通过这种方法获得的系统是原始系统的安全抽象，这意味着它至少显示了原始系统的行为[21，30]。我们将数据抽象实现为系统规范级别上的转换规范层面的抽象在抽象解释框架中得到了很好的发展[10，11，12]。实现这种数据抽象的程序转换转换了签名和过程定义。对于每个排序S，我们引入一个排序ST，它由两个构造函数S：ST和κ：S ST组成。 第一个构造函数定义一个排序值。那个骗局构造函数κ（已知）将排序为S的值提升为排序为ST的值。对于每个具体映射m：S1SnSn+1，我们定义一个映射m T：S1TSnTSnT+1在抽象分类上模仿原始分类在一般情况下，模仿通过为每个抽象映射mT提供以下重写规则来确保：mT（κ（x1），.，κ（xn））= k（m（x1，.， xn））mT（x1，.，xn）= TSn+1如果xi是TSi，对于某些i∈ {1;. ;n}过程规范的转换包括将所有变量、表达式和守卫提升到新的排序。每次出现排序为S的变量x，被ST类型的变量xT所取代，其中ST是排序S的安全抽象。类型S的表达式e的每次出现都被提升到排序为ST的表达式eT。因此，所有新引入的符号（构造函数和重写规则）都是使用并取代原来的。守卫的转换类似于表情的转换。保护g的每一次出现都被提升为布尔T类型的保护gT。在转换守卫时，我们应该确保抽象系统至少显示原始系统的行为。因此，值为κ（真）或κ（假）的守卫的行为类似于34J.R. Calamé等人/理论计算机科学电子笔记191（2007）25不→TBoolTfuncTBool：→BoolTκBool：Bool→BoolT映射和T：BoolT×BoolT→BoolTγ：布尔T→布尔varb，bJ：Boolrew和T（κ（b），κ（bJ））=κ（and（b，bJ））和 T（TBool，κ（F））=和 T（κ（F），TBool）=κ（F）和T（TBool，κ（T））=和T（ κ （ T ） ， TBool ） =TBool 和 T （ TBool ，TBool）=TBoolγ（T布尔）=T γ（κ（b））=b图三. 转换排序BoolTl−→？s（x）∈Edgl−→？s（T）−→真<$x：=T<$l∈EdgTl−→g<$ ！s（e）l∈EdgSI输入Tl−→γ（gT）<$！s（eT）<$l∈EdgTl−→g<$x：=e<$l∈Edgl−→γ（gT）<$x：=eT<$l∈EdgTSO输出TSASIGNT表2边的变换（Spec→SpecT）守卫分别评估为真或假。 警卫估计，表现as guards警卫evaluating评估totrue真.我们通过引入额外的映射来实现这一点γ：BoolTBool，每当一个守卫被评估为或为κ（true）时为true，否则为false为了避免引入不必要的非确定性，我们对排序Bool应用了一个更精细的，从技术上讲是一个非严格的转换。它的抽象，排序布尔T，如图3所示。定义5.1（混沌守卫的五月语义）守卫g被定义为函数g：→ {true，false}，混沌守卫被定义为函数gT：T→ {true，false，T}。为了将这个三值逻辑映射回二值逻辑，可以将函数γ：{真，假，T}→ {真，假}定义如下：γ（κ（真））=真，γ（κ（假））=假和γ（T）=真。在对签名进行转换并提升系统变量、表达式和保护之后，我们得到了一个仍然可以从环境中接收所有可能值的系统环境只能通过输入来获取数据。我们变换了每个输入l−→？s（x）从ennntin中提取到由适当排序的T参数化的信号的n个输入，J.R. Calamé等人/理论计算机科学电子笔记191（2007）2535不不0init≤ ∈ ∈≤M MT≤S× ××≤.Σl−→？s（x）−→真<$x：=T<$l∈EdgT（l，ηT）−→？s（T）（τl，η[Tx<$→TT]）输入Tl−→γ（gT）<$！s（e）<$l[[γ（gT）]]ηT=true[[eT]]ηT=v（l，ηT）−→！s（v）（λl，ηT）l−→γ（gT）<$x：=el [[γ（gT）]]ηT=true[[eT]]ηT=v（l，ηT）→τ（τl，ηT[x<$→v]）输出TASIGNT表3变换边的阶跃语义（SpecT→MT）(see表2中的规则SI输入T）。如前所述，对数据和输出进行处理。转换后的系统的语义由表3中的推理规则给出。给定一个IOLTS M，我们通过对M的指定应用数据抽象来导出M T。MT只能从环境中接收值，因此环境数据的无限性被压缩成一个值。基本上，转换后的系统至少显示了原始系统的痕迹，其中受环境影响的数据被值取代。这意味着，MT模拟M。 这种模拟关系现在被定义为具体的和抽象的IOLTS。 它不是一个标准的关系，因为我们允许抽象的行动。此外，我们给出了基于[21，20]的保存结果的概述。定义5.2（≤-模拟）设M1=（Σ1，Lab1，→1，σ1）且M2=（Σ2，实验2，→2，σ2）是两个IOLTS。 （≤a，≤b），其中≤a≥1×2且≤b≥Lab1×Lab2为0的情况。a模拟，i <$$> σ1，σ<$1，σ2，λ1<$σ<$2，λ2σ1≤aσ2<$σ1→λ1σ<$1<$（λ1≤bλ2<$σ<$1≤aσ<$2<$σ2→λ2σ<$2）<$，其中σ1，σ<$1 ∈ L ab，λ1∈ Lab，σ2，σ<$2∈Lab.1122我们写M1≤≤M2，如果在M1和M2之间存在这样的关系，初始状态σ12init在将变换后的系统的迹与原系统的迹联系起来之前，我们先在系统的状态和标号上定义一个序关系。为了将原始系统的状态Loc×Val与变换后系统的状态Loc×ValT联系起来，我们将关系≤S定义为：定义5.3（关系式S）设σ=（l，η）和σT=（lJ，ηT）是IOLTS的两个状态，并具有规范Spec和Spec T。：（Loc Val）（LocValT）定义为σ≤SσTil=lJx∈Var[[x]]ηT=T[[x]]ηT=κ（[x]]η）。为了将原始系统的标签Lab与变换后的系统标签LabT联系起来，我们定义了关系≤L：Lab×LabT。定义5.4（关系式L）设λLab和λTLabT。 则λLλT定义如下：• τ≤Lτ• ？s（v）≤L？s（vJ）i ≠vJ=T或vJ=κ（v）≤σa.36J.R. Calamé等人/理论计算机科学电子笔记191（2007）25⏐• ！s（v）≤L！s（vJ）i ≠vJ=T或vJ=κ（v）下面的引理陈述了M和MT之间的模拟关系（也见下图）。SpecT−a→b。2SpecT选项卡. 1标签。3M≤≤MT引理5.5设Spec是一个规范，Spec T是通过本节定义的变换从Spec获得的规范。令M和MT分别为根据表1或表3中的规则从Spec和Spec T获得的IOLTS。则M≤≤MT和（≤S，≤L）是这个模拟。证明草图：通过分别检查定义5.2中的输入和输出动作以及τ步的模拟条件来证明引理。Q在本节的其余部分，我们将这种模拟关系提升到在抽象系统和测试目的的同步产品中包含接受和拒绝的跟踪。引理5.6基于模拟（≤ S，≤ L），设M，N为IOLTS，其中M≤≤N。设P为测试目的。 则M ×P ≤≤JN ×P，其中（≤SJ，≤L）是该模拟。（σM，σP）≤SJ（σN，σP）i <$σM≤SσN且σP=σ<$P. Ther≤ L与定 义 5.4 中 的定义相同。证明草图：证明类似于引理5.5，为了考虑同步乘积而扩展。Q定义5.7（迹上的≤ -包含）设λ和ρ是IOLTS M1和M2的迹。 迹ρ ≤-包括，写作≤ ρ，i|ζ|为|ρ|且对所有i∈ {0;. ; |ζ|}。定义5.8（自动机上的≤ -包含）由IOLTS M 2 ≤ -生成的迹集包含由IOLTS M 1生成的迹集，记为[[M1]] trace≤[[M2]] trace，i对于M 1的每个迹，在M 2中存在迹ρ，使得≤ ρ。引理5.9设TP为测试目的，MSP为M与MTP的同步乘积，MS TP为MT与MTP的同步乘积。 [[MSP]]at race≤[[MSTP]]at raceand [[MSP]]rt race≤[[MSTP]]rt race。证明草图：为了证明引理，我们必须将假设1带入假设。 我们首先证明了隔离的MSP的接受和拒绝迹集是在MSTP中被接受和被恢复的唯一性的子集。这是我的梦想MSP的可接受迹线和MSTP的被拒绝迹线不具有共同的路口对于拒绝的MSP迹线和接受的MS TP迹线也显示了相同的结果。QJ.R. Calamé等人/理论计算机科学电子笔记191（2007）2537RSRS6抽象测试在本节中，我们将描述使用数据抽象进行测试选择和执行的方法。首先，我们给出了整个过程的算法概述。然后，我们描述了必要的规则系统是如何建立和测试选择和执行工作。最后，我们回顾我们的方法，并证明了合理的判决分配给一个测试执行。测试过程概述算法6.1（SelectAndExecTest（Spec，TP）：verdict∈{无、通过、不一致、未通过}）setVerdict（None）;2SpecT：=abstract（Spec）;3RS：=buildRuleSystem（Spec）;4MSTpec=基因速率LTS（SpecT）;5MTP：=generateLTS（TP）;6MCTTG：=基因速率CTG（MSTpec，MTP）;7MTTC：=选择ATC（MCTTG）;8而MTTC/=无试验病例θ（β，θ）：=NewPassTrace（notrace，θ，MTTC）;10如果（β，θ）无解在图4中，测试过程被描述为一个算法。其输入参数是规格Spec和测试目的TP。根据第5节，将规范抽象为规范T。 MSTpec由SpecT生成，MTP由TP生成。并行地，建立规则系统 包含Spec中的所有条件。稍后将需要使用具体数据来参数化测试用例。从两个IO LTS，使用TGV生成共同完成的GpMCTTG（参见图1）。 [3]）。 MCTTG可以包含到IUT的几个输出之间的选择，或者甚至在输入和输出之间的选择，因此不一定是可控的。因此，MCTTG是原系统中满足测试目的的所有测试用例的一个过度所以它可能包含导致错误判决的痕迹我们的目标是获得可参数化的测试用例（例如在TTCN-3 [13]中）以及关于数据值的信息，以实例化它们。做测试11日en12ExecTest（β，θ，notrace，MTTC）;13终止;14fi15MTTC：=选择ATC（MCTTG）;16埃利赫夫图四、测试的选择和执行38J.R. Calamé等人/理论计算机科学电子笔记191（2007）25可重复的，我们感兴趣的测试情况下，没有非确定性的选择是可能的几个输出或输入和输出之间。因此，我们选出了MCTTG的一个子图，该子图既不包含两个输出之间的选择，输入和输出之间的选择，也不是循环。我们进一步将这个子图称为抽象测试用例（ATC），表示为MTTC。尽管我们仍然在这里的IOLTS水平上工作，但我们现在必须引入参数化的变量。 在MTTC中，T的每个时现由分别参数化输入和输出的唯一的随机变量来代替。双索引对于标识状态是必要的，在该状态下，变量开始（索引i），并且在从状态i（索引j）转换时在变量集合内唯一地标识该变量。这些变量被嵌入到IOLTS的转换标签中，但在本节的其余部分中被区分为单独的Var定义6.1（可参数化测试用例）给定参数化完全测试图MCTTG（VarCTG） =（VarCTG，Lab，→CTG，σinit），参数化测试用例MTTC（VarTC）是输入完全IOLTS（VarTC，Lab，→TC，σinit），使得VarTC<$VarCTG对于MTTC和MCTTG。测试用例的状态集合是完整测试用例的状态集合的子集，并且测试用例 仅 示 出 了 在 完 整 测 试 用 例 中 可 能 存 在 的 Pas 、 Inconc 和 Fa iltac， 即 。[[MTTC]]Pas[[MCTTG]]Pas，[[MTTC]]Inconc[[MCTTG]]Inconc，andd[[MTTC]]Fail[[MCTTG]]Fail.在可参数化的测试用例可以被执行之前，它必须被实例化。这意味着，每个变量vijmtetebes tt到一个值，使得测试用例中的Pas-状态为了做到这一点，使用NewPassTrace选择Pass（图5）。如果存在这样的跟踪，则可以执行它，否则搜索下一个可能的跟踪。如果在这个抽象测试用例中找不到跟踪，则生成下一个测试用例并检查通过的跟踪。如果根本不能确定这样的跟踪，算法以最终判决None终止，而不执行任何测试用例。该算法只选择一个轨迹并执行它，必要时动态适应IUT 一个完整的测试套件包括一个以上的跟踪（不管可能的适应），可以通过引入一个循环，重复跟踪选择和执行动作来执行。 最终判定将是单次检验判定的上限（见定义2.2）。在赋值θ下执行轨迹β并不意味着这个执行在整个执行中都绑定到那个轨迹。 在测试执行期间的某个时刻，IUT可能不确定地离开预先计算的轨迹。 在这种情况下，测试执行算法试图找到另一个通过判定的跟踪。 然而，这个新的跟踪必须包含β的部分，它还没有被执行，作为它的前缀。迹赋值也只能通过新值来扩展J.R. Calamé等人/理论计算机科学电子笔记191（2007）2539O−Rs→RSRsl−→g<$ ！s（e）l∈Edgs（stat e（l，Var），stat e（l，Var），param（e））：−g.RO输出l−→？s（x）∈Edgs（stat e（l，Var），stat e（l，Var[x→Y]），param（Y））.l−→g<$x：=e<$l∈Edgτ（stat e（l，Var），stat e（l，Var[x<$→e]），param）：−g.RI输入RASIGN表4规范Spec到规则系统RS的转换建立规则体系和规则一个可参数化的测试用例可以包含由数据抽象引入的跟踪。此外，关于符号变量或它们可以被替换的具体值的关系的信息是缺失的。为了找出虚假的痕迹，并获得估值的符号变量，我们采用约束求解。我们将原始规范Spec转换为约束逻辑程序或规则系统RS。 这个规则系统构成了测试预言机或查询的基础。 将从M T T C中提取的传递跟踪β变换为查询G：β（θ）。这里，θ是数据值的可能（即有效）设置，可以用它来实例化β。设指定中的符号变量集为Varsymb。如果查询没有解决方案，则β是由数据抽象引入的虚假跟踪，我们从测试用例中删除该跟踪。如果存在解θ：Varsymb D，对于查询，β可以被映射到原始系统的轨迹我们将具有根据θ替换的符号变量的迹β称为表示为β（θ）的实例化迹。 实例化迹β（θ）是原始系统MSpec的迹。正如我们将在后面证明的那样，由β（θ）指定的结论是可靠的。知道任何一个通行证跟踪的至少一个可能的解决方案已经足够开始了执行测试用例eMTTC，并以该解θ为参数。Further，我们定义将原始规范转换为规则系统并获得查询从测试用例的通过或不一致跟踪原始规范的转换规范 由表4中给出的推理规则定义。 这些规则将规范的边缘映射到的规则。所有的规则都是rulename（stat e（l，Var），stat e（l，VarJ），para m（Y））：g. 规则的名称是，对应的动作（内部赋值为τ）。第一个状态参数根据指定位置和过程变量描述边缘的源状态。 第二个状态参数描述改变后的目标状态用同样的方式第三个参数param包含构成动作参数的规则RI输入、RO输出和ASIGN将输入、输出和内部赋值操作转换为约束规则。一个输出或一个内部动作的保护构成了相应规则的主体输入操作的规则始终有效，因为40J.R. Calamé等人/理论计算机科学电子