理论计算机科学电子笔记159（2006）187-204www.elsevier.com/locate/entcs重写逻辑中的行为组件埃纳·布洛克·约翰森，奥拉夫·奥维，阿里德湾Torjusen1挪威奥斯陆大学信息学系摘要许多分布式应用程序可以理解为在开放环境（如Internet）中交互的组件。开放环境会以不可预测的方式发生变化，因为其他应用程序可能会出现、发展或消失。为了在这样的环境中验证组件，构建反映这种高度不可预测的行为的仿真环境可能是有用的。 在本文中，验证组件相对于行为接口， 考虑了行为接口指定了对组件可观察行为的语义需求，以假设保证的方式表示。在我们的方法中，重写逻辑模型是透明的扩展与所有可观察的通信的历史，和元级策略用于指导环境行为的模拟。通过允许在可观察行为的假设范围内的任意环境行为，避免了环境的过度指定，同时验证了组件对行为接口的保证。关键词：验证，组件，行为接口，仿真策略，重写逻辑，元编程1介绍本文提出了重写逻辑的应用[17]，以测试软件单元在开放分布式环境（如Internet）中的行为开放式环境是一种存在各种其他软件单元的环境，并且很少或没有关于这些单元的信息可用。分布式环境是一种异步通信的环境。在这种情况下，推理在本质上是困难的，部分原因是非决定论1电邮地址：einarj@ifi.uio.no，olaf@ifi.uio.no，网址：aribraat@ifi.uio.no1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.069188E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187这是由分布引起的，但更典型的是由于未知和不断发展的开放环境。预测开放分布式环境中组件的行为是一个重大挑战，以确保和维护有关安全性，可用性，服务质量，鲁棒性和容错性的行为属性。系统验证的形式化方法，如霍尔逻辑、类型检查和模型检查，依赖于了解系统组件的实现细节，包括开放环境中的组件。基于测试的方法模拟了一个环境，在这个环境中系统可以进行测试运行。与验证方法相比，测试通常不能确保组件始终行为良好，但测试仍然可以揭示组件的行为然而，开放分布式环境中软件单元的一致性测试问题尚未解决[25]。本文展示了如何通过基于可观察行为的未指定形式描述来模仿开放环境，以便在建模级别验证开放分布式环境中软件单元的行为。在早期开发阶段进行基于模型的测试可以使测试过程更加有效[19]。面向对象是并发和分布式系统的主要框架，由RM-ODP推荐 [12]，并用于，例如，.Net和Corba。在本文中，我们通过对象的分布式组件进行建模，这些对象之间的消息交换是不规则的。这些模型可以在重写逻辑系统Maude [4]中执行，该系统具有模拟，模型检查和验证的功能。为了允许黑盒验证，我们在可观察行为方面使用需求规范。可观察的行为使用描述环境可用的组件服务的通用接口[13，14本文定义了一个可执行框架，用于验证开放分布式环境中模型的可观察行为。为此，在重写逻辑中捕获了异步接口，并将其与异步通信对象的标准重写逻辑模型相此外，Maude中的可执行平台以透明的方式扩展了验证设施。重写逻辑在数学上是相对的[3，5]：可以在重写逻辑本身内部对相对重写进行形式化推理，并在MaudeMeta级别执行相对规范。反射的使用是必不可少的，我们的方法，允许引导搜索和系统监控的模块化，可组合和分层的方式。反射可以用来定义可执行对象模型的执行策略，例如[15]中提出的非确定性执行策略。相关规范支持分层体系结构，E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187189可以在每个级别上给出具体说明。反射可以用于扩展系统模型，例如，[24]第二十四话。在本文中，我们透明地扩展了可执行规范，其历史上可观察到的通信在元级，并定义执行策略在元级的指导下的通信历史的要求。一种策略用于模拟开放环境，另一种用于测试可执行模型。这两种策略相结合，以使一个假设保证风格的基于模型的测试组件的行为接口。论文概述：第2节介绍了行为接口的形式主义。节3介绍了重写逻辑和Maude工具。节4开发了用于监控和测试可执行Maude模型的元级策略。 在第5节中介绍了一种模拟开放环境的策略，并展示了如何在测试场景中使用这种策略。第6节讨论了有关工作和今后的工作。2行为接口开放分布式系统（ODS）可以由并行运行并通过远程方法调用进行异步通信的组件或对象表示。组件的实现细节可能是未知的，在这种情况下，推理必须依赖于系统组件的抽象规范。我们假设组件配备了指导我们如何使用它们的通用接口。由于一个组件可以用于多种用途，因此它可以配备多个接口。本节提出了一种形式主义的观点的基础上，一般接口的概念与行为的要求，限于安全方面。有关这项工作的更多细节，请参见[13，14]。并发组件的黑盒规范可以用可观察的行为来表示，即，输入和输出到组件的时间序列。这与封装的概念非常吻合;只有可见的操作才被考虑在规范级别。执行可以由一系列通信事件表示，这在非终止执行的情况下是无限的。然而，无限序列并不容易推理。为了避免无限序列，规范可以用执行的有限初始段来表示，在执行过程中捕获组件的抽象状态。这些层序通常被称为历史[6]或迹[11]。预闭执行集表达了Alpern和Schneider意义上的安全属性[1]。有限序列。我们考虑由类型T参数化的有限序列的抽象数据类型Seq[T]。将定义190E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187利用收敛的方程组，以空序列ε和右附加_;_：Seq[T]×T→Seq[T]为序列构造子.我们用“_“表示一个具有多个旋转的函数的规则集合。我们定义了投影，_/_：Seq[T]×Set[T]→Seq[T]，以及一个ε/S=ε εewS=假（t;x）/S=ifx∈Sthen（t/S）;xelset/S（t;x）ewS=x∈S符号#t表示序列t的长度，并以类似的方式定义。2.1语义设Ob是对象标识符的无界集合。设Data是一组数据值，包括Ob。在本文中，我们通常让o1，o2∈Ob。通信事件具有以下形式从o1到o2的消息其中msg由Data组成。这一项被认为是o1的输出事件和o2的输入事件。对于可观测事件，o1和o2是不同的。对象o的可观测输入和输出事件的集合分别表示为INo和OUTo它们的联合表示为INOUTO。对象o的字母表是INOUTo的子集。o的字母表可以覆盖o的通信的某些方面。在下一节中，我们将介绍静态定义的字母表的语法。迹集Tα<$Seq[α]是一个一个良好格式序列的预闭集。定义2.1一个特殊项Γ是一个三元组的集合，其中（1）o∈Ob是一个对象标识符，（2）α是o的一个可能无限字母表，（3）T是α上的一个迹集。对于任何指定Γ，我们可以导出对象与Γ的对象通信的通信环境E（Γ）。在ODS设置中，我们通常认为通信环境是无限的。由于规范Γ不需要覆盖o行为的所有方面，我们说Γ是（o的）接口规范。下面我们考虑面向对象的分布式系统，其中通信是通过远程方法调用实现的。为了实现异步通信，我们通过两个事件对方法调用进行建模：表示调用发起的事件和表示其E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187191建成设Mtd是一个无界的方法名集合，m∈Mtd.对于o1对o2的方法m的调用，初始化事件由调用者o1生成，从o1到o2用invoc（m）表示，完成事件由被调用者o2生成，从o2到o1用comp（m）表示。为了简化阐述，我们抽象的参数值在本文中。为了增加可读性，我们用o1→o2.m表示这些事件，o1←o2.m。当我们考虑异步通信对象时，调用者可能在（被动地）等待完成时通信，而被调用者可能在执行方法时通信。因此，在任何给定呼叫的发起和完成之间可以观察到其他事件当我们考虑可观察行为的历史时，每个完成事件都必须在相应的调用之前，这就产生了以下通信历史的良构性概念：wf（ε）=truewf（t;（o→oJ.m））=wf（t）wf（t;（o<$oJ.m））=wf（t）<$#（t/o→oJ.m）≥#（t/o<$oJ.m）其中#（t/o→oJ.m）是跟踪t的长度，该跟踪t被限制为从o到oJ的方法m的调用事件，对于完成事件也是如此。定义2.2A的具体值αo，α，T 关于Refines 另一种规格如果αJ<$α且<$t∈ T， . t/αJ∈ T J。因此，在{ t/α j}的意义上，精化对应于投影迹集上的子集关系|t∈T }<$TJ.请注意，一个规范可以用（部分）不相交的字母表来细化几个规范。规范的组合可以被引入来定义分布式服务意义上的部分组件或系统方面[13，14]。2.2语法接口规范可以以通用方式给出。通用规范被称为行为接口。一个对象可以支持多个接口。由于Maude没有提供一个语法来指定可观察的行为，静态定义的字母表，也没有方法（甚至没有Full Maude），我们通过面向对象的接口引入了一个可观察行为的语法：接口F（配置上下文参数）继承F1，F2，.，Fm开始192E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187J有cointerfaceop m1（.. . ）...op mn（.. . ）本地跟踪上的指定其中辅助函数定义>端接口可以有上下文参数，这些参数通常描述最小化环境，表示支持接口的对象所需的静态链接。初始化和完成事件与每个方法声明相关联（范围包括方法参数，本文将忽略这些参数）。在指定公式中，关键字相互依赖。让对象通过接口来类型化。通过为调用者标识一个类型，即协接口，我们限制了可能调用该接口方法的对象，同时允许该对象调用协接口方法。这为在方法执行期间与调用方的交互打开了大门。在实现语言中，对调用者的访问可以通过Maude中的显式参数来提供，也可以通过Creol [15]中的隐式参数来提供。协接口在异步设置中提供强类型。从语义上讲，协接口声明增加了接口的字母表，因为添加了与协接口方法相关的事件。传承接口允许多重继承，但不允许循环继承图.在子接口中，可以声明额外的方法和行为约束。共接口限制适用于本地声明的方法。如果接口F是用继承子句声明的，那么超接口的字母表将包含在F的字母表中。当被限制为超接口的相关字母时，跟踪集通过交集继承。因此，一个接口总是会细化它的超接口。定义2.3对象o相对于接口F的接口字母表，记为αo：F，定义为以下形式的事件集：(i) invoc（m）从oJ到o和comp（m）从o到oJ，对于在F中声明的m，(ii) 在共同接口中声明（或由共同接口继承）的从o到oJ的invoc（m）和对于m从oJ到o的comp（m）(iii) αo：FJ中的任何事件 其中F是F的超界面。定义2.4设F，F1，.，Fn与相应的指定谓词P，P1，.，Pn，且h在历史上变化。如果F继承E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187193F1， . . . ，Fn，F的非线性性质为P（h）≠P1（h/αthis：F1）你. . . . n（h/αthis：Fn）.假设担保谓词。在ODS中，对象所处的环境会发生变化，而规范与环境的假设行为有关。我们将假设保证规范风格[16]适应于可观察行为的设置。假设应表达对输入的限制和对输出的保证。然而，由于对输出的要求可能取决于早期输入，而对输入的要求可能取决于早期输出，因此通常难以分别制定假设和保证。相反，我们使用单个谓词P来关联输入和输出事件，并从P中提取假设部分和保证部分：定义2.5让IN和OUT表示该接口的输入和输出事件集。假设保证谓词是从规范P（h）中推导出来的，其中假设部分A和保证部分G由以下等式A（ε）=trueA（h;x）=A（h）<$（x∈IN<$P（h）<$P（h;x））G（ε）=trueG（h;x）=G（h）<$（A（h;x）<$P（h;x））由规范specP（h）给出的迹集是{h|G（h）}。注意，两个集合{h|G（h）和{h|A（h）}是预闭的，它们的交集是{ h}中包含的最大（预闭）迹集|P（h）}。假设是环境中对象的责任。的假设部分确保每个输入都是可接受的，假设没有更早的违规。保证是支持接口的对象的责任;当假设成立时，它们得到保证。保证部分确保每个输出是可接受的，假设假设成立。因此，需要一个实际的环境来细化A给出的轨迹集，需要一个接口的实现来细化G给出的轨迹集。2.3示例：最小接口行为界面通过用餐哲学家的例子来说明。桌子对象告知哲学家哲学家左边邻居的身份，并提供食物单位。一个哲学家可以借他邻居的钱，然后还回去。哲学家之间的互动，194E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187该表受接口限制。这导致了内部方法和可由协同接口类型化的其他对象外部使用的方法之间的明显区别。在这里，每个哲学家都有一个盘子，必须在吃饭前向邻居借一个。因此，哲学家有主动行为和被动行为。强类型和协接口保证了只有哲学家才能调用这些方法。接口Phil接口表开始与Phil杆式座椅（外邻：菲尔）操作返回坚持操作吃产品规格根据协同接口的要求，由调用者在此Phil对象的环境中指定任意Phil对象。菲尔的字母表是由事件给出的：caller→this. stickcaller←this. stickthis→caller. stickthis←caller. stick和类似的事件。我们定义了以下规范，菲尔：规格0≤借出（h）≤1规格0≤借入（h）+请求（h）≤1wherelent （ h ） =# （ h/←this.borrowStick ） −#（h/→this.returnSti ck）borrowed（h）=#（h/this←Stick）−#（h/this→returnStick）requested（h）=#（h/this → Stick）− #（h/this ← Stick）在这里，lent捕获借给邻居的棒的数量，borrowed捕获对象从其邻居借用的棒的数量，reques- ted捕获未完成的借用请求的数量。这三个功能是根据迄今为止可观察行为的历史来定义的。指定意味着一个布尔变量可以跟踪分发的棍子。因此，规范的假设部分简化为APhil（h;x）=APhil（h）<$（x∈ {→this.returnStick}<$lent（h）>0）说明环境归还的树枝不能多于它所借的树枝。上面两个接口通过引入接口Eat- ingPhil连接，继承Phil，并以Table作为参数，从而提供E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187195初步的环境知识。哲学家必须有两根棍子吃，这一点加强了对菲尔接口EatingPhil（table：Table）继承Phil开始标准进食量（h）借出量（h）= 0借入量（h）= 1其中eating（h）=#（h/this←eat）>#（h/this→eat）端在这里，吃是真的，当这个物体能够吃的时候。这个接口并没有加强从菲尔继承的假设，即，AEatingPhil（h）=APhil（h）=hJ≤h·lent（hJ）≥0.3重写逻辑与莫德本节简要介绍重写逻辑[17]和Maude [4]。 重写理论是一个4元组R=（E，E，L，R），其中签名E定义了语言的函数符号，E定义了术语之间的等式，L是一组标签，R是一组标签重写规则。从计算的观点来看，重写规则t-→tJ可以被解释为允许模式t的实例演变成模式tJ的对应实例的局部转换规则。重写规则适用于状态配置的片段。如果重写规则可以应用于配置的非重叠片段，则转换可以并行执行。因此，重写逻辑（RL）是一种容易捕获并发更改的逻辑。许多并发模型已经成功地在RL中表示[4，17]，包括Petri网，CCS，Actors和Unity。非正式地说，RL中的状态配置是给定类型的多项集，在（成员资格）方程逻辑（E，E）中指定，RL的函数子语言支持OBJ风格的代数规范分类表示一个术语属于一个给定的类别。当对计算系统建模时，配置可以包括由等式逻辑中定义的不同类型的术语建模的不同系统组件。一个RL对象是一个term对象：|a1：v1，. ，an：vnn n，其中O是对象的标识符，C是它的类，aiV1RL通过重写规则扩展了代数规范技术，以捕获系统的动态行为，补充了定义术语语言的方程。假设所有的项都可以归约为标准形式，重写规则将项转换为E的方程的模。重写规则可以196E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187有一个条件（重写、等式和成员资格的结合），它必须满足主规则才能应用。 每个规则描述了配置的一部分如何在一个过渡步骤中演变rl[label]：子配置−→子配置crl[label]：subconfiguration−→subconfiguration ifcondition一个以if-then-else表达式作为右手边的无条件规则也可以作为两个互补的条件规则给出。RL中的规则可以在高抽象级别上制定，非常类似于组合操作语义[18]。Maude系统支持RL规范的分析。3.1反射和莫德元水平重写逻辑是反射性的，因为存在一个无限呈现的重写理论U，它是普适的：任何无限呈现的重写理论R（包括U本身）都可以在U中表示。设C和CJ为配置，R为重写规则集。我们写R <$C→Cj来表示重写理论R中C可以重写为CJ。非正式地，配置C和RL中规范的重写规则的集合R可以由元级的项C和R表示。使用这个符号，我们有等价性[3]：R C → CJ惠UR，C → R，Cj，其指出，如果项C可以重写为重写理论R中的项CJ，则在通用重写理论U中，R中的C的元表示，R，R，Cj，可以重写为R中的CJ的元表示，R，R，CJ，R，Cj。Maude包括元表示重写理论R和通过所谓的下降函数将规则从R应用于术语C的元表示的设施。元级重写规则可用于从R中选择哪个规则应用于C的哪个子项。这是通过定义一个解释器函数来完成的，该函数以一个有限呈现的重写理论R、一个项C和一个确定性策略S作为参数。元级重写规则可以进一步用于修改重写理论的配置或规则集因此，元级重写可以用作重写理论R周围的包装器，以便抽象地模仿更精细的重写理论RJ扩展R。关于RL和Maude中反射的理论和使用的进一步细节可以在[3，4，5]中找到。E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187197rl[req-stick]：X：Ob|饥饿：真，myS：是，nbrS：否，：nbr：Y −→X：Ob |hungry：true，myS：yes，nbrS：req，nbr：Y（从X到Y的invoc（'InvowStick））。rl[borrow]：X：Ob |hungry：false，myS：yes，nbrS：s，nbr：Y（invoc（X：Ob |hungry：false，myS：no，nbrS：s，nbr：Y（comp（'wStick）from X to Z）.rl[rcv-stick]：X：Ob |hungry：true，myS：yes，nbrS：req，nbr：Y（comp（X：Ob|饿：真，我：是，是。rl[eat-req]：X：Ob|饥饿：真，myS：是，nbrS：是，nbr：Y −→X：Ob |hungry：true，myS：yes，nbrS：yes，nbr：Y（invoc（'eat）from X to 'table）.rl[eat]：X：Ob |hungry：true，myS：yes，nbrS：yes，nbr：是（comp（X：Ob |hungry：false，myS：yes，nbrS：no，nbr：Y（invoc（'returnStick）from X to Y）.图1.重写捕捉哲学家行为的规则。3.2示例：哲学家我们引入一个Maude规范，它实现了2.3节中给出的EatingPhil规范。设O是一个在Ob上变化的变量，哲学家对象被定义为RL对象：|hungry：_，myS：_，nbrS：_，nbr：_.布尔属性hungry表示哲学家是否饥饿，属性myS和nbrS表示其筷子的状态（yes，no，req），用于对指定施加同步约束，nbr标识邻居。哲学家通过消息传递与环境异步交互。内部行为表现为哲学家（不定时地）向自己传递信息。图中给出了从规范中选择的规则。1.一、4监视和测试可执行模型可执行模型的可观察行为可以通过记录模型执行的通信历史来监控：这可以在Maude元级的帮助下透明我们可以进一步测试执行是否符合模型的行为规范，方法是定义元级谓词，这些谓词对记录的历史进行操作，并在发生违规时阻止执行为了在元级别执行规范，我们开发了一个自定义策略;即，重写适用于模型的元表示的规则因此198E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187crl[exec-monitor]：MetaRep |curTerm：T，curModule：MOD，labels：L LS，failedRules：FR历史：H如果RES：：Result4Tuple，MetaRep |curTerm：getTerm（RES），curModule：MOD，labels：LS L，failedRules：nilHistory：H ; getNewMessages（T，getTerm（RES），MOD，H）其他MetaRep |curTerm：T，curModule：MOD，labels：LS L，failedRules：FR L公司历史：H公司if RES：=metaXapply（[MOD]，T，L，none，0，unbounded，0）<$#FR≤ #LS.图2.元级重写策略S监视器记录通信历史。操作RES：：Result4Tuple表示绑定到RES的重写成功，使用RES：= term形式的条件将项绑定到RES。可以在重写之间检查当前状态。这使我们能够在执行规范时记录通信历史：我们可以通过比较规则应用前后配置的元级表示来检查重写规则的应用是否导致新消息的发射。对象名称：MetaRep |curTerm：_，curModule：_，labels：_，failedRules：_curl用于存储控制连续元级重写所需的信息。cur- Term包含当前配置的元表示，curMod- ule是对象级模块名称的元表示，其中将执行重写，labels是来自此模块的规则标签列表，failedRules包含不适用于curTerm的规则的标签列表。对象HISTORY：_HISTORY有一个属性h，它包含在运行时作为消息列表记录的实际通信历史。该对象与对象级模型的对象不同，因此不被对象级规范中的任何重写规则修改，也不需要应用。自 定 义 策 略 S监视器 被 实 现 为 条 件 重 写 规 则 exec ：MetaRep×History→MetaRep×History（见图2）。实际的重写是由内置 的Maude 函 数 metaXapply 完 成 的 ， 该 函 数返 回 一 个 元 组 ， 使 用getTerm从该元组中获得重写项。请注意，Maude中的空格表示列表连接：如果L是标签，LS是标签列表，则L LS是非空标签列表。该策略以循环方式将标签列表中的规则应用于curTerm中的元级别配置（在[15]中给出了基于伪随机数生成器的随机规则选择的位置公平策略。）如果没有适用的规则，执行将终止。辅助函数getNewMessages将项T与新系统配置进行比较，即，将标记为L的规则应用于T的结果。如果在新的系统配置中有新的通信消息，则历史对象的属性h用新E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187199充分和传播如果有多个新消息，则这些消息是由并发操作引起的，因此可以以任意顺序添加到历史记录中。策略S测试是通过扩展S监视器来定义的，该监视器具有检查给定规则应用是否会导致非法状态的功能，如谓词参数所指定的。我们考虑由行为接口定义的通信历史上的谓词。为了获得一个组合系统，全局历史上的谓词将被公式化为许多行为接口的需求规范的结合，可能与不同的对象相关联。特定对象的行为规范由全局历史上的谓词表示，仅限于可能通信事件的适当子集。一旦系统试图达到违反全局历史谓词的非法状态，S测试测试针对特定对象o和行为规范Tα，测试谓词可以表示为P（h）=h/α∈ Tα。 对于行为要求设为谓词P：Seq[α]→Bool，由收敛方程组定义通过针对当前全局历史h减小P（h/α），迹集中的成员资格是有效可计算的。S测试策略在Maude中通过扩展条件exec规则来实现，该规则具有一个分支，该分支在每个重写步骤之间检查给定的谓词，并且如果谓词被违反则阻止执行。Maude函数CheckPredicate：Pred×MsgList→Bool用于此目的。一个被预测对象是使用一个常数H来指定的，该常数H充当实际通信历史。在运行时，CheckPredicate根据实际历史分析谓词如果执行被策略阻止，记录的历史记录会提供系统运行的错误跟踪，描述如何违反规范。例4.1哲学家根据EatingPhil接口（2.3节）的行为可以接受的行为可以用Maude算子AccBeh表示：eqAccBeh（nil）=trueeqAccBeh（H ; MSG from X to Y）=P（H/X ; MSG from X toY）其中P是EatingPhil接口的指定谓词，其中符号h/X表示h/INOUTX。由于Maude规范中的P是一个跨越所有对象的全局谓词，因此不需要将对象标识符作为单独的参数传递给AccBeh。此外，由于AccBeh对每个输入和输出事件进行增量检查，因此我们不需要使用第2.1节中定义的保证和假设部分2.2.200E.B. Johnsen等人/理论计算机科学电子笔记159（2006）1875开放测试环境的模拟可以模拟一个开放的环境，使得抽象对象的行为完全由行为接口定义。对可观察行为的接口假设可用于在假设谓词施加的限制5.1开放环境在对象级，重写理论被用来在语法上模拟未知的环境。在开放环境中，对象可以在执行期间动态地创建和销毁。为了模拟开放环境，我们定义了一个包含一组（抽象）对象标识符的术语，这些对象标识符表示当前可能与系统交互的对象：中文（简体）|absID：_，sysID：_，seed：__。absID集将用于生成系统对象的输入消息。 系统对象被表示为一组sysID对Obj×Set[Mtds]，其中包括对象标识符和对应于对象接口字母表的方法名称集。抽象对象发出的消息被输入到系统的真实对象。seed属性用于消息生成。为了从环境中的对象向系统生成任意但语法正确的输入，我们需要从sysID中选择一个对象o，并向o生成一条消息（要么调用o接口中可用的方法，要么回复历史中找到的o的调用）。为此，我们使用伪随机数生成器[15]，并让函数next：Nat→Nat为环境产生新的种子值让函数genMsg：Obj×Obj×Set[Msg]×Nat→Msg从环境中的对象向系统中具有字母表α的对象o生成新消息msg，使得msg∈α。消息生成的重写规则由下式给出：rl[msg-gen]：环境|absID：o1A，sysID：（o2，α）C，seed：X−→中文（简体）|absID：o1A，sysID：（o2，α）C，seed：next（X）搜索genMsg（o1，o2，α，X）5.2开放测试环境的语义模拟在元层，使用重写理论对未知环境进行语义模拟.开放环境的最低行为要求由系统接口中的假设给出。定义一个元级策略Srestrict，它限制重写系统根据可观察行为的谓词进行行为。此策略类似于S测试，但当应用启用的规则会违反谓词时，S测试会E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187201规则集：配置：MetalevelS限制（P1（h/α1））P2（h/α2）检验↓对照品R1和R 2R1→ R2，（ C1C2），历史：h↑历史记录器C1C 2重写系统：对象级别重写系统：图3.开放环境中可观察行为的相对测试Srestrict将尝试MetaRep对象的标签开放环境不会终止;如果没有重写规则适用于curTerm的任何位置，则策略会更改种子值并重试规则。抽象的环境规范现在可以用作实际编程组件的测试平台（见图3）。设R1是一组对象级的重写规则，用于生成（可能还有垃圾收集）消息。来自R1的规则可以应用于由Envir对象组成的配置C1设R2为对象级重写规则集，适用于配置C2中的具体对象，例如，给定的组件，在内部状态上具有同步约束。设α1和α2分别是与对象C1和C2 相关联的字母表，使得α1<$α2。设P1和P2分别是观测上指定环境和实际组件的谓词.如果考虑多个接口，P1将是假设的结合，P2将是保证的结合，仅限于相关的字母表。元级策略Srestrict将规则应用从R1限制到可接受的环境行为，提供了一个抽象的、开放的环境，该环境可以以不违反谓词P1的任何方式行为。我们本文结合了两种元级策略，它们对谓词的违反有不同的反应：Srestrict将限制规则的应用，使通信历史符合谓词;Stest将在谓词不成立时停止执行并产生一个错误对象。通过指定一个谓词，它只跨越来自组件对象的消息，另一个谓词跨越所有对象，并使用Stest执行前者，使用Srestrict执行后者，我们可以测试编程组件是否正确执行，前提是环境正确执行。5.3哲学家的榜样这个测试场景是在Maude中通过定义一个类似于图2中给出的规则的元级重写规则exec-test来实现的，它结合了上面描述的S 限 制和S 测 试使用了metallevel规格202E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187测试第3.2节中描述的哲学家的实现。测试配置包括一个具体的哲学家对象，一个表对象的规则，以及一个由4个抽象哲学家组成的环境，如第二节所述。5.1. 哲学家行为的重写规则（图）。1）与Phil接口规范（第2.3节）进行了比较，使用S检验，而msg-gen规则的应用受到S限制策略的限制，以符合假设APhil。当这个非终止性规范的执行测试规则的应用数量被限制为5000时，结果（在53494167次重写之后）是涉及具体对象的355条消息的踪迹我们观察到，如果引入了违反保证规范的规则，则该策略将检测到违规行为此外，如果环境假设被打破（例如，通过将假设谓词替换为空假设真），这将导致也将被检测到的对保证规范的违反6相关和未来的工作我们并不打算在这里全面调查有关监测和测试的大量文献。许多以前的基于历史[8，19，22]和基于自动机[2，21，23]的方法需要定义特定和确定性的测试用例。相反，我们使用随机测试和假设保证规范来捕获开放环境，其中环境行为在假设谓词的范围内是任意的。最近在[9]中提出了与我们的S限制对于开放环境，在最小假设范围内的随机测试似乎比确定性测试更有吸引力。本文中考虑的可观察行为的规范在重写逻辑中相当容易实现。所考虑的具体化语言可以被更有表现力的语言所取代。例如，将我们的开放环境建模方法与有限轨迹上的线性时间时态逻辑规范结合起来会很有趣。在[20]中给出了重写逻辑中验证这类公式的一个有效算法。7结论本文的主要贡献是通过扩展Maude模型，E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187203具有可观察行为和相关执行策略的概念。本文展示了开放环境的抽象规范如何在一个扩展了行为接口的重写逻辑模型中非常自然地被捕获。行为接口表达了对组件的可观测性的安全需求。该方法是在基于方法的、面向对象的设置中提出的，但可以很容易地调整为通用的异步消息传递。由于Maude支持的重写逻辑的响应特性，可以在元级别定义执行策略。在本文中，我们使用了四种方式的这种设施。首先，一种策略被定义为非确定性地生成系统的任意输入。其次，定义了一种策略，以透明地引入对一组通信事件的监控。第三，定义了一种策略，通过对可观察行为的语义要求来限制系统输入。结合这些策略，可以在最小假设的范围内模拟开放环境的任意行为。对象级和元级约束的分离便于对环境进行不同假设的实验。同样的方法也可以用于执行由其可观察行为定义的原型模型，然后再决定其实现细节。第四，定义一种策略来测试可执行模型是否在可观察行为的语义需求方面表现良好。结合所有四种策略，我们获得了组件或分布式应用程序模型的抽象验证环境，其中环境是未指定的，但受到最小的观察要求。致谢。我们非常感谢Eyvind W。感谢阿克塞尔森为实现这些想法做出的贡献，感谢匿名裁判提供了有益的意见。引用[1] 阿尔彭湾和F. B. Schneider，Defining liveness，Information Processing Letters21（1985），pp. 181比185[2] Barbey ， S. ， D. Buchs 和 C.Péraire， 面向对象软件的基 于 规 范 的 测 试 理 论 ， 在 ： Proc 。Dependency Computing Conf.（EDCC2），LNCS 1150（1996），pp. 303- 320[3] Clavel ，M.， “Reflection in Rewriting Logic: Metalogical Foundations and MetaprogrammingApplications,” CSLI Publications, Stanford, California,[4] Clavel ， M. ， F. Duran ， S. Eker ， P. Lincoln ， N. Martí-Oliet ， J. Meseguer 和 J. F.Quesada ， Maude ： Specification and Programming in Rewriting Logic ， TheoreticalComputer Science 285（2002）. 187-243[5] Clavel， M. Meseguer，Reperception in conditional rewriting logic， Theoretical ComputerScience285（2002），pp. 245-288204E.B. Johnsen等人/理论计算机科学电子笔记159（2006）187[6] 达尔，O. J.，程序证明可以实现吗？，in：M. Amirchahy和D. Néel，editors，Les Fondementsde la Programmation，Institut de Recherche57比114[7] 达尔，O. J.， “可验证编程”，Prentice Hall，纽约，纽约，一九九二年[8] Doong，R.K. 和p.G. 陈晓，面向对象程序的测试方法，北京：计算机科学出版社，2000。工程师，Methodol。3（1994），pp. 101-130[9] Duran，F.，M. Roldán和A. Vallecillo，Invariant-driven strategies for Maude，ENTCS124（2005）. 17-28，Proc. 4th Intl.重写和编程中的减少策略讲习班（WRS 2004）。[10] Goguen，J. A.，T. Winkler，J. Meseguer，K. Futatsugi和J. - P. Jouannaud，IntroducingOBJ，in：J. A. Goguen和G. Malcolm，editors，Software Engineering with OBJ：AlgebrasSpecification in Action，Kluwer，2000 pp. 3-167[11] 霍尔角 A. R.， “Communicating Sequential Processes,” Prentice Hall,[12] 国际电信联盟，开放分布式处理-参考模型第1-4部分[13] Johnsen，E.B. 和O.Owe，A composite formalism for object viewp
我的内容管理
展开
