基于模AC的异步通信对象模型测试及验证方法研究-挪威奥斯陆大学计算机科学系

理论计算机科学电子笔记264（2010）69-84www.elsevier.com/locate/entcs使用模AC重写的异步通信对象模型测试Olaf Owe，Martin Ste Escheren，and Arild B.托尔胡森挪威奥斯陆大学计算机科学系摘要由于非确定性，开放环境中异步通信对象的测试和验证具有挑战性。我们通过提出一种接口规范语言来探索黑盒测试的正式方法，该语言对对象的行为进行了一种约束-承诺风格的描述。该方法适用于克理奥尔对象。Creol是一种高级的面向对象的建模语言，因此我们对行为模型进行基于模型的测试。通过同步执行规范和受试组件来完成测试。由于通信的异步性质，测试应达到观察等效性。这导致了测试用例的可达状态空间的大量增加。我们减少了状态空间，通过使用设施重写模AC（结合性和交换性）内置到重写逻辑系统Maude，并探索状态空间的广度优先搜索。我们目前的实验结果表明，这种方法的实用性关键词：测试和验证，异步方法调用，活动对象，重写逻辑，形式语义。1介绍系统测试是保证软件和系统可靠性和质量所不可或缺的。许多不同的测试方法和框架已经被提出，并投入（良好）使用多年。形式化方法和程序语言理论已经被证明是有价值的，使测试实践成为一个更正式、更系统的学科（参见。例如[16，2]）。形式化的测试方法近年来获得了发展势头，例如基于模型的测试趋势[12，4]。在以前的工作[19]中，我们提出了一种正式的方法，用于在开放环境中对异步通信组件进行基于黑盒规范的测试这项工作的一部分得到了欧盟项目IST-33826Credo：分布式服务进化结构，HATS：使用形式化方法的高度适应性和可信赖的软件（http://www.hats-project.eu），以及德国-挪威DAAD-NWO交换项目Avabi（异步活动对象行为接口的自动验证）的支持。1571-0661 © 2010 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2010.12.01570O. Owe等人理论计算机科学电子笔记264（2010）69以及测试框架的实现。在本文中，我们将展示如何扩展的方法来验证组件和目前的实验结果表明，我们的方法的实用性。我们在Creol [11，27]的上下文中这样做，Creol是一种用于分布式系统的高级面向对象面向对象是一个自然的选择，因为对象建模是RM-ODP推荐的开放分布式系统的基本方法[24]。对于这样的系统，异步通信模型是有利的，因为它使调用者和被调用者并行，从而避免了不必要的等待方法返回。不利的一面是，不确定性使验证和测试模型更具挑战性。在异步系统中，由于网络或排队引起的通信延迟可能导致消息超越，由此产生的非确定性导致状态空间爆炸。人们普遍认为，处理复杂系统的方法是考虑与其环境交互的组件从内部执行中抽象出来，Creol组件的黑盒行为由它们接口上的交互给出。我们使用一个简洁的语言在通信标签来指定组件和组件的预期行为是作为一组在接口上的痕迹。输入和输出的相互作用都是特定的，但扮演着非常不同的角色。由于输入事件不受对象的控制，因此输入被认为是对环境的假设，而输出描述了对象的承诺。这种在组件控制下的交互和来自环境的交互之间的关注点分离，通过定义有效的可观察输出行为，假设一定的调度，导致了组件行为的约束-承诺风格规范对于输入交互，我们确保通过按指定顺序调度传入呼叫来满足对环境的指定假设，而对于由组件控制的输出事件，我们测试事件是否按指定发生。组件的调度和测试是通过将组件的执行与规范同步来完成的因此，在组件的执行中强制执行调度，并且根据规范中的输出事件测试组件这提供了一个框架，用于测试组件的实现是否符合接口规范。测试框架会将组件在给定调度下的错误行为报告为错误由于消息延迟和超越，来自组件的传出消息被外部观察者观察到的顺序不一定反映它们实际发送的顺序。测试是基于在接口处可观察到的行为，因此传出通信的顺序不应影响测试结果。规范语言的操作语义通过将输出事件的某些重新排序视为观察等效来考虑通信模型的异步性质，并在观察等效的情况下进行测试。输出事件的重新排序可以通过将输出事件的序列定义为关联的和可交换的来表示。我们认为我们的测试框架O. Owe等人理论计算机科学电子笔记264（2010）6971特别适合于实现这一点，因为使用重写逻辑系统Maude，可以使用等式属性来声明结合性和交换性[9]这是一个非常好的方法来评估这些问题。本文扩展了[19]，它介绍并给出了我们在这里进一步探索的测试方法的正式基础，主要贡献是：验证我们在重写器Maude中提供了一个实现，并使用Maude的搜索功能进行状态探索（用于重写模AC）以验证组件，并研究Maude内置的AC推理支持如何有助于在实验结果我们提出了使用Maude重写工具的实验结果，该工具提供了我们方法的好处的经验证据。我们比较，在两个系列的实验中，在状态空间上的influence的使用，ING莫德的内置AC支持对所有可能的输出事件的重新排序的显式表示。在测试异步通信对象时，使用AC重写可以大大减少资源消耗。AC重写在时间和重写次数方面付出了巨大的代价我们在第2节中回顾了克里奥尔语的形式化，必要时重复了以前论文中的一些技术细节。相应的行为接口规范语言以及如何将其用于测试的解释在第3节中给出。在第4节中，我们描述了该理论的可执行实现。实验结果见Sect. 五、2Creol建模语言我们正式Creol，一个高层次的，面向对象的建模语言的分布式系统，Creol功能的活动对象和异步方法调用。与基于多线程的面向对象语言（如Java或C#）相比，该语言的特点是活动对象。活动的单位是对象;每个过程都属于一个对象，活动不跨越对象边界。通信基于异步交换消息，并且在存在发送消息但不接受消息的语言手段的意义上是不对称的：对象总是能够输入的。因此，在方法调用的被调用方，每个对象都拥有一个输入“队列”，在该队列中，传入的消息等待该对象提供服务。为了避免不受控制的干扰，每个对象都充当监视器;在每个时间点上最多执行一个方法体。 默认情况下，选择输入队列中的哪个方法调用下一个进入对象是不确定的。在抽象语法之后，我们勾画了操作语义，集中在外部行为上，即，与环境的信息交换。72O. Owe等人理论计算机科学电子笔记264（2010）69C：：= 0| CC| ν（n：T）.C|c [（女，男）] |o [c，F，L]|非线性分量F：：= l = f，.. .，l=菲尔德M = l = m，. ..，l= m方法组m：：= λ（n：T）.λ（x：T，.，x：T）.t方法f：：=（n：T）.λ（）.v|n（n：T）.λ（）. λn'场t：：= v|停止|让x：T = e在测试线程中e：：= t|如果v=v，则e，否则e|if（v.l（））theneelse eexpr.|v @ l（v）|五.l（五）|v.l（）|v.l：= λ（s：T）.λ（）.v|新的n|claim @（n，n）|获取@ n|暂停|抓斗|释放（n）v：：= x|n|（）价值观L：：= 100|T锁定状态表1抽象语法2.1语法抽象的语法，在标准的对象演算的风格，是在Tab。1.一、名称n表示对类、对象和线程的引用。为了便于阅读，我们允许自己写o及其语法变体来表示引用对象的名称，c表示类，n表示非特定的名称。 组件C是类、对象和（命名的）线程的集合，0表示空组件。组件的子实体是使用并行构造的子实体组合而成的。并行执行的实体是命名的线程，其中t是正在执行的代码，n是线程的名称。线程的名字n同时也是未来的引用，在这个引用下，t的结果值（如果有的话）将是可用的。在本文中，我们限制自己的情况下，该组件仅由一个对象，加上任意多个线程。一个类c[（F，M）]带有一个名字c，并在F和M中定义了它的域和方法。一个标识为o的对象o[c，F，L]保持对它实例化的类c的引用，存储其字段的当前值F，并维护一个二进制锁L，指示对象内当前是否有任何代码是活动的（在这种情况下锁被占用）或没有（在这种情况下锁是空闲的）。符号T和分别表示锁被占用或被释放。命名的线程并不是“执行中”的方法体的化身每个线程都属于它执行的“内部”特定对象，即，它可以访问哪些实例变量。内置对象锁用于排除对对象状态的不受保护的并发访问：尽管每个对象可能有多个方法体化身部分求值，但在每个时间点，这些方法体中最多有一个（锁所有者）可以在对象内活动。ν-运算符用于隐藏和动态作用域，如π-演算所知除了组件之外，语法还指定了较低级别的语法结构，特别是方法，表达式和（未命名的）线程，它们基本上是表达式的序列。后面的表达式claim、get、suspend、grab和release处理同步。它们负责适当地释放和获取对象的锁。所有的特性和它们的表示都是非常标准的，并且（除了通过方法调用的通信）在接口上不可见，我们在这里省略了更多的细节，并参考技术报告[20]。O. Owe等人理论计算机科学电子笔记264（2010）69732.2操作语义被测试程序的操作语义分两个阶段给出：步骤内部的程序，以及那些发生在接口。内部规则处理不与对象环境交互的步骤更有趣和相关的是“外部”规则，通过交换通信标签来描述组件与其环境的交互。通信标签是界面交互的基本构建块，在表1中给出。二、 组件或对象通过调用和返回标签与环境交换信息，交互是传入的或传出的（标记为？resp. ！）。标签ncallo.l（v）n表示对象o中方法l的调用。在该标签中，n是标识执行被调用方中的方法的线程的名称，因此是（未来）引用，在该引用下，方法调用的结果将对调用方可用（如果有的话）。传入的标签nreturn（v）？将相应调用的值传递回对象，使其可以读取。它的对端，即输出返回，将值传递给环境。除此之外，标签可以通过形式为ν（n：T）的绑定来前缀，该绑定表示所传输的名称的新鲜度，即，范围挤压。.界面行为由规则给出，就像Tab一样。3（我们展示了四条规则中的两条，处理传入通信，缺少的两条用于传出通信）。外部步骤作为以下形式的过渡给出：C−→a 如果您的帐户已被删除，请重新登录。在步骤之前和之后，分别为C。特别是，上下文包含了到目前为止已知的对象和线程的标识，以及相应的类型信息。该信息在传入通信步骤中被检查，并且在执行步骤（输入或输出）时被更新这两个操作由以下符号Ξ►a:Tand Ξ +a(1)这构成了Tab中规则前提的一部分。3 .第三章。直观地说，它们的意思如下：标签a是格式良好且类型良好的wrt。该信息是指异步调用，该异步调用导致类型T的值。（1）的右边表示法通过作为label的一部分传输的绑定扩展了绑定上下文a适当。由于篇幅所限，我们在这里省略了正式的定义。直观地说，它们确保只有类型良好的通信才能发生，并且在还原过程中上下文保持最新。 规则C所有我处理来电，和γ：：= ncalln.l（v）|n返回（n）|ν（n：T）.γ基本标号a：：=γ？ |γ！输入输出标号表2结构化通信标签74O. Owe等人理论计算机科学电子笔记264（2010）69a=ν（ε′）。 我不知道。l（v）？Ξ►a:TΞ´=Ξ+aC所有ICl（o）（v）inrelease（o）;xa=ν（ε′）。 nreturn（v）？刘慧卿：好的'=RET Ia'Ξ►C−→ Ξ►Cǁn⟨v⟩表3外部步骤基本上，与程序的其余部分并行地添加新线程n（其同时表示最终结果的未来引用）。符号M.l（o）（v）表示将实际值传递到方法体t，其中s是从那条小巷里出来。Wewrite1C1=t2的内部和外部步骤，以<$2<$C2，展示t作为外部步骤的痕迹。3一种行为接口规范语言对象在特定执行中的行为在接口上由Tab给出的一系列标签描述。二、 因此，一个对象的黑盒行为可以用一组轨迹来描述，每个轨迹由一个有限序列组成标签。这对于由一组对象组成的组件也是一样的。为了指定标签跟踪的集合，我们采用了一种简单的跟踪语言，带有前缀，选择和递归。表4包含其语法。规范语言中标签的语法自然非常类似于Tab的标签。二、比较选项卡。在图2和图4中，有两个区别：第一，这里的规范语言使用变量，而不是名称或引用n。第二，这里的标记允许（x：T）.γ形式的结合，其在表1中没有类似物。2;形式ν（x：T）.γ当然对应于ν（n：T）.γ。这两个绑定构造都充当变量声明，不同之处在于ν（x：T）.γ不仅引入了一个变量，而且还断言该变量所表示的名称必须是新鲜的。绑定（x：T）.γ对应于一个常规的变量声明，引入了表示任意值的变量xTab中给出的语法。4允许指定轨迹集。然而，并非所有的规范都有意义。我们通过引入γ：：= x调用x.l（x）|xreturn（x）|v（x：T）.γ|（x：T）.γ基本标号a：：=γ？ |γ！输入输出标号：：= X|ϵ| a. ϕ |+|建议X.产品规格表4规范语言O. Owe等人理论计算机科学电子笔记264（2010）6975限制：类型：传递的值必须对应于该方法的预期类型;作用域：变量必须在使用之前声明;以及通信模式：在接口处看到匹配的传出调用之前，不能返回值。此外，我们注意考虑规格的极性。在规范中，区分输入和输出交互是很重要的，因为输入消息是在环境的控制下，而输出是由指定的对象提供的。这将规范分为环境责任下的假设部分和由组件控制的承诺部分为了指定非确定性行为，语言支持选择运算符，我们区分环境所采取的选择-外部选择-和对象所负责的选择 尤其是，我们不允许所谓的混合选择。参见[20]关于这些限制的形式化的细节，现在只需要注意，规范必须是良构的，并且规范：wfp代表相应的判断。 元变量p（表示极性）代表？，！，或？！，在哪表示空序列或过程变量的极性，以及？还有！分别表示格式良好输入和输出规范3.1观测模糊Creol对象异步通信，并且在通信期间可能不保留消息的顺序外部观察者或测试者观察到的顺序并不一定反映消息发送的顺序，因此，观察到的“错误”通信顺序不应被视为错误，我们必须将具体化放宽到某种适当的观察等效概念，由观察五、请注意，目的不是重建某种“正确”的交流顺序。 当测试一个组件时，我们控制通信，测试规范和框架扮演着环境（生成CUT的输入）和观察者（控制输出）的角色，但是为了测试可观察性，我们希望保留外部视角。在测试给定对象时，我们指定对象使用输入的顺序，而不是它们生成的时间。通过这种方式，我们指定了对象的输入调度，这使得我们的指定比模糊输入的情况更具表现力。同时，我们指定从环境中看到的对象的输出。因此，我们模糊了输出，而不是输入。此设置允许同步并行合成。输入模糊在其他设置中可能是有益的，并且例如已经应用于基于霍尔逻辑的克里奥尔语的推理系统[14]中。在所提出的组合推理系统中，消息生成被认为是可观察的，但不是消息消费。因此，在该系统中，输入是模糊的，但输出不是。规则Eq-SWITCH捕获了通信的异步性质，因为传出通信的顺序不起作用。规则EQ-PLUS允许在非确定性选择上分配输出。规则EQ-REC表示递归定义的标准展开。规范语言的操作语义是直接的归约。76O. Owe等人理论计算机科学电子笔记264（2010）69ν（ν）。γ1！.γ2！.ϕ≡obsν(Ξ).γ2！.γ1！.ϕ► （1+2）：wf！Eq-S开关γ！. （1+2）看起来像是个大笨蛋γ！.1+ γ！. ϕ2EQ-PLUSrecX. [recX. /X]Eq-REC表5观察等效性塔阿► a4σbBΞ►C−→ Ξ►CΞ►Cǁϕ−→ Ξ►C´ǁϕPAR-INT1<$1<$C<$$>−→<$1<$C<$σPAR周杰伦：wf？Ξ►ν(Ξ′). （Cnl etx：T=o. l（v）int）−→ERR-CALL周杰伦：wf？′ERR-RETΞ►ν(Ξ). （Cnv）−→表6平行组成3.2对象的异步测试表6定义了接口规范与组件的交互，基本上是嵌入式系统和组件都必须参与相应的步骤，对于传入的通信，调度与组件交互的顺序，而对于传出的通信，只有当它匹配规范中的传出标签时，交互才会发生，并且如果规范需要输入，则会引发错误。组件可以通过内部步骤自行进行（参见规则PAR-1NT）。规则PAR要求，为了继续，组件和规范必须参与“相同”的这里► a4σb表示存在一个替换σ，使得组件产生的标签a和接口描述指定的标签b可以matched.请注意，在成功应用PAR规则后，指定中的变量可能已被具体值取代。我们省略了匹配的细节，并参考技术报告[20]。规则ERR-CALL和ERR-RET报告错误，如果指定需要输入作为下一步，而对象可以进行输出，无论是调用还是返回。在规则中，错误指示错误的发生。注意，根据规则Eq-SWITCH，等价关系允许输出的重新排序，但不允许输入的重新排序。4Creol的规范驱动解释器Creol的操作语义在重写逻辑[31]中被形式化，并且可以在Maude重写引擎[8]上执行，这给出了Creol的解释器。我们O. Owe等人理论计算机科学电子笔记264（2010）6977用于测试Creol组件的可执行框架包括：在重写逻辑中形式化的规范语言和Creol解释器的修改版本。我们通过同步指定项和对象之间的通信来获得用于测试的指定驱动解释器。组件的输入是在规范的范围内非确定性地生成的，同时测试对象的输出行为是否符合规范，与标准解释器相比，内部活动没有修改。Creol的默认行为是将传入的方法调用放入被调用方的输入队列中，从该队列中不确定地选择要执行的调用。对于指定驱动的解释器，如果传入的调用被指定并且对象的锁是自由的，则相应的方法代码应该立即开始执行。在实现中，传入的消息直接从规范中生成Maude中Creol模型的标准模拟通过与解释器一起重写初始模型配置来实现。Maude为了测试组件，我们从模型中提取一个对象及其类定义，而不是使用初始配置作为输入。这将成为被测组件（CUT）。CUT，它的规范和修改后的解释器然后由Maude重写。因此，可以测试来自大型模型的选定对象的特定行为属性。标准的Creol状态配置（Cfg）是对象、类和消息的多集合，转换的Maude重写规则的形式为rlCfg =>Cfg 对于规范驱动的解释器，我们为规范引入术语Spec。阳离子并在表单上添加规则（等级库||0）Cfg =>（规格“||O'）Cfg'相对于Spec测试对象O，其中||表示同步并行合成。每一条规则都演化出一个规范的状态和一个对象以同步的方式：仅当交互与规范中的互补标签匹配时才发生交互。例如，在一个示例中，选项卡中PAR规则。6是由几个Maude规则实现的，用于可能发生的不同类型的通信事件。我们请读者参考[19]中的一些例子。在实现中，我们通过在输出标签前缀为输出指定的情况下将前缀运算符声明为AC来定义关联和交换（AC）输出与Maude规则一起，实现了选择的分布（上述规则Eq-PLUS），这使得测试框架能够进行高达观察等效性的测试。5实验结果本节描述了两个系列的实验，使用的是前一节中的实现模板。实验证明了该方法的实用性：使用AC重写可以大大减少资源消耗，测试异步通信对象时。AC重写在时间和重写次数方面付出了巨大的代价。至于状态空间，效果并不那么明确。78O. Owe等人理论计算机科学电子笔记264（2010）69第一个例子是量身定制的，以显示一个简单组件的效果第二个例子是企业应用程序集成领域中已知的“贷款报价示例”的抽象版本这些示例还说明了如何使用接口规范语言来测试组件行为，以及如何通过Maude的搜索命令使用模型检查来实现对具有跟踪规范的组件的验证当使用search命令时，Maude不仅探索一个跟踪，而且探索由组件给出的一组行为 系统通常会探索一组轨迹，而不是仅仅一个，原因如下：首先，探索一个轨迹（平凡地）意味着探索所有前缀;当然，这不仅适用于使用Maude其次，规范可能包含非确定性（除了组件也可能表现为非确定性的事实之外最后，在我们的上下文中最重要的是，一个痕迹总是意味着“观察模糊”，如Tab中所五、为了测量AC重写的效果，两个系列的实验进行两次，或者AC重写接通，或者不接通。当规格的AC等效性被切换为非AC时，我们使用规格的等效但扩展版本来比较结果。在第一个例子中，被测组件由一个对象和n个方法m1到mn组成。该规范规定，在任何方法可以返回之前，必须调用所有方法。在Creol中，这是通过结合处理器释放点和等待保护来实现的[27]。3个方法的行为规范如下：c3=n1，则称c.m1（x1）为n？. n2n=c.m2（x2）n？. n3 n .（n1return（y1）！. n2return（y2）！. n3return（y3）！）. ϵ这 是 一 种 通 过 使 用 Maudecommnd ： rew （ 第 3 行 ） 来 实 现 的 灵 活 方 法 ||c）cClass。，其中c表示Creol对象。Maude重写配置，或者在组件即将执行未指定的输出，或者在没有更多规则应用时停止。在后一种情况下，如果原始规范被完全消耗，这就证明了组件符合规范，在这个意义上，c的测试执行只会导致规范c3预见的输出。这种一致性关系类似于[35]的输入-输出一致性关系（ioco）定义5.1Letout（t后的t）表示在执行跟踪t后由t指定的所有可能的输出事件的集合。让（c after t）表示组件c在执行t之后的可能输出事件的集合。设迹（traces）是指定的迹的集合。我们的一致性关系conf定义如下：c conf优惠deft∈traces（t）：out（c after t）out（t后）根据方法调用启动的线程的内部交错，可能会产生不同的结果。MaudeO. Owe等人理论计算机科学电子笔记264（2010）6979C315.000毫秒10.0005.00003 4 5 6 7 8非AC AC图1.一、验证c是否有AC重写。在可达状态空间中对错误配置进行广度优先搜索：搜索结果：BTC3||ccClass =>+ϕ||conf errorMsg（S：String）.通过改变指定中输入标签的顺序，我们可以很容易地检查输入的不同调度如何影响对象的执行例如，在一个示例中，搜索对于来自指定的错误状态，其中调用的顺序是m1，m3，和m2没有给出解决方案，这意味着按照这个顺序调用的方法，组件不会不符合规范。图1中绘制的两个数据系列显示了在有或没有AC重写的情况下探索状态空间所需的时间，其中n是方法的数量。这些数据表明，使用AC重写时，重写次数的增加远远小于使用规范的等效扩展版本。在第二个例子中，代理充当客户端和某些服务的几个提供者之间的中介（参见[23]）。最初，我们考虑一个经纪人，在客户要求这样做后，查询一个固定数量的提供商的（价格）报价，并返回一个答案给客户，给出最好的选择。经纪人查询两个服务提供商的规范可以给出：如果b=nc1，则调用b.getP（x）？ .（n1）调用p1.getQ（x）！. n2callp2.getQ（x）！）. n1返回（v1）. n2返回（v2）n？.nc1return（v）！. - 是的请注意，尽管前面的示例说明了生成对组件的传入调用和测试来自组件的传出返回，但此示例还包括测试传出调用和生成传入返回。对于传入的返回，测试框架生成伪随机的、类型正确的返回值。对于这种规范，如果代理组件在接收到来自客户端的调用之前调用提供者，并且在完成与提供者的交互之前返回来自客户端的初始调用，则代理组件将是不符合规范的。在开放的环境中，代理知道的提供者的数量可能n毫秒CPU时间AC非AC3164743837951981.49861.0306.78275.40749.311827.894NA9153.316NA80O. Owe等人理论计算机科学电子笔记264（2010）69MS3002001003 4 5 6 7 8 9k值非AC AC图二. 代理组件随着时间的推移而变化，因此我们假设经纪人将被新的提供商通知，并与他们建立联系，以及失去与其他人的联系。代理的一个进一步开发的版本支持这一点，它允许客户端在将响应作为getP方法调用的参数之前给出代理必须查询的提供者的数量。方法getP现在接受两个参数，请求报价的服务的名称，以及代理应该联系的提供者的数量。为了验证这个新代理的行为，我们使用以下形式的一系列规范：bk=nc 1 .（供应商注册）。（n1）调用p1.getQ（x）！. ... . nkcallpk.getQ（x）！） .n1返回（v1）.............. nkreturn（vk）？. nc1return（v）！.你好，其中k是供应商的数量。图2分别绘制了AC重写的时间。针对k的6结论我们已经提出了一个形式化的并发面向对象语言和行为规范语言，异步通信对象的测试和验证。由于网络属性，可能会发生通信事件的重新排序。我们的方法描述了一种处理这种情况的方法，即通过定义输出事件的重写规范模AC。这种方法的一个优点是，我们可以精确地定义输入的调度，并测试对象的内部同步属性。当评估我们的方法的实验案例研究，我们得到的证据表明，使用模AC重写使我们能够覆盖更广泛的测试用例比我们可以这样做。Creol模型的测试也与C或Java等语言中的实现测试相关：首先，间接地，由于分布式系统中固有的许多形式的非确定性可以通过关联性和交换性形式化，因此我们的结果也与其他具有异步可比较性的语言相关K毫秒CPU时间AC非AC31343421735331016482577631.96588617.7969106NAO. Owe等人理论计算机科学电子笔记264（2010）6981通信，以及观察等效性的替代定义。其次，更直接地，在[22]和[1]中，它显示了如何使用不同的测试技术来检查Creol模型和C实现的工业分布式系统之间的一致性。在[22]中，动态符号执行技术用于测试Creol模型与实现之间的一致性。使用相同的案例研究，[1]的作者展示了如何对现有的Creol模型进行测试。AASP-C用于将事件记录点插入SuT的现有代码中。该模型同样装有同步点。测试程序用于重放模型中记录的事件，并与测试程序记录的事件同步，仅当相应事件记录在SuT中时，才允许因此，可以验证实现和Creol模型的一致性。将这些方法与我们用于验证Creol模型和规范之间一致性的方法相结合，可以产生一种针对规范的实现一致性测试方法。6.1相关工作系统测试是保证软件和系统质量必不可少的。[6]提出了一种集成面向对象程序的黑盒和白盒测试的方法等价性是基于可观察的等价项和基本对作为测试用例的想法，但不是在异步设置中。Godefroid等人[18]描述了如何在基于约束的编程语言的上下文中实现输入序列的状态空间约简。提出了一种测试算法，该算法通过从预定义集合中非确定地选择输入事件来系统地生成所有可能的行为。通过利用约束语言无法在观察上区分无序输入集的排列，减少了组合爆炸，并提出了一种更有效的测试算法。与我们的方法的一个主要区别是，状态空间中的减少来自约束程序本身的结构，而不是来自通信事件的交换性测试过程由状态空间探索工具VeriSoft [17]驱动。该论文[13]描述了基于将组分与规格相结合的组分分析。此外，VeriSoft用于假设/保证规范的有界模型检查，内置的部分降阶有助于分析的效率然而，无论是对象交互模型，共享变量，和规格，不变的基础上，使用霍尔逻辑，从我们的不同。在[3]中，假设被用作驱动单个组件进行单元测试的环境LTS用于对组件的行为进行建模。这项工作的一个有趣的特点，在我们的缺席，是技术自动生成的假设，一个组件需要对环境的一些属性举行。文献[7]以Petri网和OBJ为基础，研究了基于同步序列的并发面向对象程序的测试。在他的论文[29]中，Long提出了ConAn（82O. Owe等人理论计算机科学电子笔记264（2010）69从测试脚本。该方法允许指定组件方法调用的序列以及调用应该发出的顺序（参见[30，33]）。为了安排预期的顺序，使用外部时钟，引入测试的目的。在[25]中全面介绍的NModel框架，为C#提供了基于模型的分析和基于模型的测试，其中抽象模型，通常是面向对象程序的转换系统，用于测试。与之相关并同样由微软开发的是Spec Explorer方法（及其前身AsmLT），一种用于测试反应式面向对象程序的工具。在模型程序的基础上，例如，在Spec#规范语言中，是“模型自动机”，它可以被看作是接口自动机和抽象状态机（ASM）的组合，用于测试用例生成。处理非确定性，模型将可观察和可控制的动作分开，类似于我们在规范语言中区分输入和输出动作。依靠博弈论的基础，他们的一致性概念是基于交替模拟，而不是比较痕迹，在这项工作中。为了处理大型且可能有限的状态空间，Spec Explorer使用不同的抽象和修剪技术。一种是基于通过识别被认为是等价的状态（“状态分组”，参见“状态分组”）来构建模型自动机的商[21]和[5]）。这些状态分组对应于模型检查中已知的谓词抽象，并且与这里提出的可观察等价性具有类似的目的也就是说，用于减少状态空间，但是是用户给定的，并且由于异步通信而不是专门捕获可观察到的等效状态。有关Spec Explorer的详细讨论以及该上下文中进一步结果的链接，请参见[37]。另一种成熟的功能测试方法是输入/输出一致性测试（简称ioco）[34，35]。Ioco是基于输入输出转换系统的，我们的一致性关系是密切相关的。在[36]中研究了使用ioco测试理论的基于顺应性的测试和上下文测试。许多测试工具都是基于ioco测试理论的变体，例如TGV，TEST GEN和TorX。在ioco测试的背景下，[15]使用符号转换系统来解决状态爆炸问题。参与者的单元测试框架，即，主动并发对象的概念在[10]中提出，使用基于离散事件的仿真环境OPNET。重写逻辑中指定的组件接口的验证也是[26]的主题[32]认为克里奥尔和调查对象活动的不同限制的行为重点是对象内部调度，以及作为对象内部状态断言的测试目的。这与我们对接口通信的关注形成对比。6.2今后工作Creol已成功地用于模拟复杂和高度动态的通信系统，例如。[28]中的无线传感器网络，其中使用Ad hoc按需距离矢量（AODV）路由算法作为案例研究。ASK是一个工业规模的多线程异步应用程序，用于连接人们。ASK的很大一部分是用克里奥尔语建模的[1]。这两个模型都是COM-O. Owe等人理论计算机科学电子笔记264（2010）6983丛Creol和面向对象编程语言的相似性，以及Creol的表达能力允许模型在结构上接近AODV算法。问系统本身。这就需要对模型进行测试。我们目前正致力于将我们的方法应用于AODV模型的Creol模型的基于模型的测试。确认我们感谢Rudolf Schlatte对Creol应用程序测试的深入了解，以及对相关工作的建设性批评和提示的匿名评审引用[1] Bernhard Aichherig，Andreas Griesmayer，Rudolf Schlatte，and Andries Stam.使用Creol建模和测试多线程异步系统在TTSS爱思唯尔，2009年。[2] G.伯诺Testing against formal specification：A theoretical view.在Samson Abramsky和T. S. E. Maibaum编辑，TAPSOFTSpringer，1991年。[3] C.布伦德尔，D。Giannakopoulou和C. S.帕萨雷亚努假设保证测试。在SAVCBS'05的会议记录中[4] M.布罗伊湾J. Jonsson，P. Katoen，M. Leucker和A. Pretschner，编辑。基于模型的反应系统测试，LNCS第3472卷。Springer，2005.[5] 科林·坎贝尔和马格斯·维恩斯多个状态分组的状态探索。在ASM算法，复杂性和逻辑实验室，巴黎12大学，2005年。[6] H. Y. Chen，T. H. Tse，F. T. Chan和T. Y. 尘 黑白：面向对象程序类级测试的集成方法。ACM软件工程与方法学报，7（3）：250[7] 霍燕辰，孙玉霞，T。H.阿谢并发面向对象软件测试中同步序列的选择策略在COMPSACIEEE计算机科学出版社，2003年。[8] M anuelCl avel 、 Francis coDurran 、 StevenEker 、 Patri ckLi ncol n 、 NarcisoM art′s-Oliett 、 Jos′eMeseguer和Carolyn Talcott。Maude 2.0系统2003年RTA，LNCS第2706卷。Springer，2003年6月[9] M anuelCl avel 、 Francis coDurran 、 StevenEker 、 Patri ckLi ncol n 、 NarcisoM art′s-Oliett 、 Jos′eMeseguer和Carolyn Talcott。Maude手册（版本2.1.1）。SRI International，Menlo Park，2005年4月。[10] Mark E.斯科特·科因作者：Kenneth M. Hopkinson，and Stuart H.库考斯基 在专有的基于离散事件的模拟中单元测试参与者的方法。在WSC2008年冬季模拟会议[11] 克里奥尔语。 http://heim.ifi.uio.no/creol。[12] S. R. Dalal，A. Jain，N. Karunanithi，J. M.利顿角M. Lott，G. C. Patton，和B. M.霍洛维茨基于模型的测试在实践中 在proc 1999年国际 软件工程会议，1999年。[13] 尤尔根·丁格尔计算机辅助假设/保证推理。第25届国际软件工程会议（ICSE[14] Johan Dovland Einar Broch Johnsen和Olaf Owe动态系统的可观察行为：并发对象的组件推理。在FInCo爱思唯尔，2008年。[15] Lars Frantzen，Jan Tretmans和Tim A. C.威姆斯基于符号规范的测试生成。Grabowski和B. Nielsen，editors，FATES 2004，pages 1[16] 玛 丽 · 克 劳 德 · 戈 德 尔 测 试 也 可 以 是 正 式 的 。 在 彼 得 ·D. Mosses 、 Mogens Nielsen 和 Michael I.Schwarzbach，编辑，TAPSOFT '95会议录Springer，1995年。[17]帕特里斯·戈德弗鲁德使用VeriSoft对编程语言进行模型检查。在POPL '97的会议记录ACM，1997年1月。84O. Owe等人理论计算机科学电子笔记264（2010）69[18] Patric e Godefroid，L. 贾加迪河 是的，K。 Léaufer. 一种通用的数据系统，用于基于约束的交互式服务。在SIGSOFT FSE中。ACM，2000年。[19] Immo Grabe，Marcel Kyas，Martin Ste Geden，and Arild B. 托尤森 用于测试异步Creol组件的可执行接口规范。在FSENSpringer，2010.[20] Immo Grabe，Marcel Kyas，Martin Ste Baglien，and Arild Braathen Torjusen.用于测试异步Creol组件的可执行接口规范。Tech.第375号报告，奥斯陆大学，2008年7月。[21] W. Grieskamp，Y. Gurevitch，W. Schulte和M.维恩斯为抽象状态机生成有限状态机。在ISSTAACM，2002年。[22] Andreas Griesmayer，Bernhard Aichernig，Einar Broch Johnsen，and Rudolf Schlatte.分布式并发对象的动态符号执行FMOODS/FORTESpringer，2009年6月。[23] 格雷戈尔·霍佩和鲍比·伍尔夫。企业集成模式：设计、构建和部署消息传递解决方案。Addison-Wes