理论计算机科学电子笔记150（2006）143-157www.elsevier.com/locate/entcs协调模型基于分布式对象检索的形式化模型卡罗琳湖Talcott塔尔科特1，2计算机科学实验室Menlo Park，CA 94025，美国摘要我们提出了一个家庭的分布式对象系统表示不同的意见，与不同的意见之间的细化关系的协调模型。我们从通过异步消息传递进行交互的分布式对象开始。这样一个系统的语义是一组事件偏序（事件图），给出了可能的系统执行期间的交互。全局协调要求是对允许的事件图的约束。系统协调规范由一个元级协调器组成，它根据给定的全局策略控制系统中的消息传递。可以使用用于不相交子系统的协调器来细化/分布系统范围的协调，所述不相交子系统与它们的对等体通信以实施全局策略。通过进一步的变换，元级可以由通过控制器对象进行通信的系统变换的基本级对象代替。使用分布式对象反射的反射俄罗斯娃娃模型，在重写逻辑中形式化了协调模型。 用几个例子说明了一般思想。保留字：协调，分布式对象反射，策略，事件图1引言我们目前正在进行的工作，开发语义模型的协调分布对象系统和正式的可执行规范，从多个1该方法旨在让更多的用户感受到公平竞争。本工作部分得到了NSF拨款CCR-023446的支持。2Email：clt@ c s. 这是一个很好的选择。埃杜乌1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.028144C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）143观点。这些观点的范围从一个对象系统之间可能的相互作用的全局视图到控制器对象如何实现协调的局部视图。前者可以被认为是一个端到端的需求水平。后者更接近于系统设计或实现。最终的目标是一个理论的细化和组成的协调分布式对象系统。底层计算模型基于通过异步消息传递进行交互的分布式对象的Actor模型[15，5，1]。这种系统的语义是一组事件偏序，称为事件diagram[14，9，26]。可执行规范在重写逻辑[18，20]中使用分布式对象重写的递归俄罗斯娃娃（RRD）模型[19]进行形式化。在此设置中，协调要求是对允许的事件图的约束。通过指定由元级协调器对象执行的协调策略来指定系统范围的协调器，该元级协调器对象根据该策略控制系统中的消息传递。可以使用用于不相交子系统的协调器来分布系统范围的协调，所述不相交子系统与它们的对等体通信以实施系统范围的策略。元级可以由通过控制器对象进行通信的系统转换的基本级对象代替。计划第2节简要介绍重写逻辑和RRD模型。第3节定义了事件模型以及协调器和协调需求的概念。第4节定义了协调器的基于策略的可执行规范以及满足协调要求的协调策略的概念第5节讨论了将系统范围的协调器分发到多个本地协调器，以及删除元级以支持对象级控制器的转换。第6节讨论了一些相关的工作，第7节最后讨论了未来的方向。2背景为了提供上下文，我们简要介绍了重写逻辑和分布式对象重写的相关俄罗斯娃娃（RRD）模型重写逻辑[18]是一种逻辑形式主义，旨在对并发和分布式系统进行建模和推理[17]。它基于两个简单的思想：系统的状态表示为代数数据类型的元素;系统的行为由系统状态之间的局部转换给出。重写规则描述的状态。重写规则的形式为t≠tJifc，其中t和tJ是表示系统状态的局部部分的项，c是关于t的变量的条件。这条规则说，当系统有一个C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）143145子组件匹配t，使得c成立，则子组件可以演变到tJ，可能与由匹配系统状态的其他部分的规则描述的改变同时发生。重写规则的应用过程生成计算（也被认为是扣除）。Maude [7，8]是一种基于重写逻辑的形式化语言和工具集，用于开发，原型设计和分析形式化规范。RRD（Replicative Russian Dolls）[19]是一个基于重写逻辑的分布式对象响应该模型将逻辑反射与分布式对象的结构化相结合，作为可以推理和控制其子对象的元对象（a la Russian Dolls）的嵌套配置。该模型可用于开发交互的正式规范以及分布式基于对象的系统的架构和行为方面。例如，因特网不是真正的互联网，而是具有不同网络域的网络的网络，除了通过特定网关、防火墙等之外，这些网络域不能直接访问。作为另一个示例，多媒体服务器是资源管理器对象（负载平衡、准入控制、对象放置等）和执行环境对象的嵌套集合，该执行环境对象协调生成媒体流的所包含对象的执行。为了指定和建模协调，我们使用两大类元对象协调器和定制器。协调器有一个独特的属性，它拥有对象和消息的嵌套配置，并控制其所包含配置中消息的传递。定制器包含单个对象，用于在本地管理对象元数据和调整对象通信。3事件图和协调要求我们使用类似Maude的语法来描述形式化模型。对象被形式化为以下形式的项：[a：A|atts|输入，输出]其中a是对象标识符，A是类标识符，atts是属性集，给出对象的内部状态。inQ和outQ是对象输入和输出消息队列。为了简单起见，我们假设消息的格式为a-mb，其中a是消息目标（收件人），mb是消息正文。单个对象的行为由以下形式的消息传递重写规则给出：rl[dlv]：[a：A|atts|（msg inQ），outQ]=>[a：A|阿茨山|inQ，（outQ outQ '）] 如果条件146C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）1430输入队列的第一条消息（msg）被传递。因此，对象术语cond是一个布尔术语，用于约束规则适用的3一个对象系统是一个多组对象和消息，具有默认的通信基础设施规则[obj.out]和[obj.in]，这些规则简单地将消息从输出队列移动到系统soup，并将消息从系统soup移动到目标参与者的输入队列。4rl[obj.out]：[a：A|阿茨山|inQ，（msgoutQ）] =>[a：A|阿茨山|inQ，outQ]消息rl[obj.in]：[a：A|阿茨山|inQ，outQ] msg =>[a：A|阿茨山|（inQ msg），outQ] if target（msg）== a当规则左侧匹配一个子多集并且规则条件的对应实例（如果有的话）评估为真时，诸如消息传递和通信规则之类的规则应用于对象和消息的多集。在这种情况下，匹配的子多重集被替换为规则右侧的相应实例。计算是一个可能无限的重写序列：S−→l1 . . .−→lkSK...其中L1是由所应用的重写规则、递送规则或基础设施通信规则之一确定的标签对于使用传递规则的重写，标签具有dlv（a-mb，i，b，j）的形式，其中a-mb是传递的消息，i是对象本地时间（建模为发送或接收的消息的数量），b，j是使用发送者标识符和本地时间表示的消息标识符。为了将计算中记录的额外信息形式化，我们用一个代表对象本地时间的计数器来记录每个对象，并通过用发送对象标识符和本地时间来注释汤中的消息来增强通信规则。 因为我们允许一次发送多条消息，所以在时间j发送的消息所生成的第i条消息的发送时间是j +i。事件图语义。与计算相关的事件图是事件（mb，a，i，b，j）的集合，使得dlv（a-mb，i，b，j）是 重写计算。事件的偏序是传递的3一般来说，也可以创建新对象。 为了简化讨论，我们省略了这个方面。4这里我们考虑封闭系统。将这些思想扩展到开放系统是很简单的，在开放系统中，消息可以从外部对象到达，也可以通过添加外部交互规则发送到外部对象。C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）143147关闭抵达和激活订单。到达顺序表示消息传递到给定对象的顺序。它是由(mb，a，i，b，j）<（mb'，a，i'，b'，j'） 如果<我。激活顺序是导致消息发送的消息传递与这些消息的传递之间的因果顺序。它是由(mb'，b，j，a '、j'）<（mb，a，i，b，j''）如果<在标记为dlv（
[c：Coord| {S [a：A|atts |nil，nil，j+ k，ready]M}，策略：P，事件：ed|输入，输出]如果k：= length（mQ）/|M：= mkPend（mQ，a，j）其中，mkPend（mQ，a，j）是未决事件的集合（b-mb：a，j+i），使得b-mb：a，j+i是mQ的第i个元素，从0开始计数。规则[obj.in]由[coord.in]取代，仅在满足政策时适用。rl[coord.in][c：Coord| {S（[c：Coord| {S [a：A|atts|（a<-mb），nil，j+1，busy]策略：P，事件：（ed e）|输入，输出]ifed，pend（S），（a<-mb：b，i）|= P/\e：=（mb，a，j，b，i）其中pend（S）是S中的未决事件的集合。150C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）143我们可以从规则中看到，协调器维护对象输入队列中最多有一个消息的不变量，以便可以确定导致输出队列中消息当一个对象的输入队列为nil且其状态为busy时，这表明消息已经被传递，因此输出队列中的消息可以被转换为挂起事件，并且本地时间可以被递增。如果状态为就绪，则表示对象正在等待下一条消息的传递。在协调系统的计算中，如果（a-m：b，j）在未决事件中，则激活前驱事件（具有形式（此外，如果（mb，a，j，b，i）在events属性中，则对象a的本地时间大于j。定义：协调系统事件图。协调系统C[c，P]{S}（S中的对象具有空输入）的事件图语义l1li并且输出队列）被定义为流。 L etπ=C0−→C1. . . −→Ci. . . e是对C0= C[c，P]{S}的计算，并且令ed i是协调器在第i个状态中的事件属性的值。那么与π相关联的事件图，EDS（π）是有限事件集EDS（π）=i∈Nat埃德岛Defn：策略满足要求。 我们说策略P满足协调要求Φ（写为P| = Φ）如果对 于 C[c ， P]{S} 的 每 个 计 算 π ， π 的事 件图 满 足Φ ， 形 式上 写为 Φ （ ED S（π））。协调政策现在，我们给出满足第3节末尾给出的示例要求的策略的示例。政策示例1. 用于协调与自动收报机的通信的策略P+（t）由以下等式（ed，M，（[c：Coord| {S}，策略：P，事件：ed，sent：M（x-mb：b，i），fwd：locs| inQ, outQ c’<-dlv((x<-mb : b,i), c)]if c’ := lookup(locs,x) /\ c’ =/= c当dlv消息到达时，所包含的挂起事件被添加到配置中（rulecoord.xrcv）。rl[coord.xrcv]：[c：Coord| {S}，策略：P，事件：ed，发送：M，转发：locs|（c-dlv<（（[c：Coord|{S（a<-mb：x，i）}，策略：P，事件：ed，发送：M，转发：locs|输入，输出]在股票代码系统协调的情况下，这是足够的。包含自动收报机的协调器只需要本地事件来检查策略，而发送到其他对象的消息不受约束。对于组通信的例子，需要进一步的适应，以确保每个协调器有足够的信息，以作出正确的排序策略决定。实现此目的的一种方法是使用一组消息标识符（发送者、发送时间）来扩展未决事件的注释，这些消息标识符对应于必须在未决消息之前交付的消息。例如，在第五种情况下，由待处理事件发送者错误发送的所有消息的消息标识符的集合是足够的。然后，可以调整fifo策略，以仅使用扩展注释和本地事件图来确定满意度。一般来说，注释和策略适配可以作为全局协调器的转换来完成，并且一旦决策被本地化，则全局协调器可以被分发用于自动收报机系统。首先本地化意味着验证本地化是否正确的工作可以在一个抽象级别上进行，而不是同时处理级别交叉。C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）1431535.2通过对象级控制器进行为了消除元级嵌套，协调器可以由控制器对象代替，其中基本对象适于经由控制器通信这种转换不依赖于策略或对象系统。每个协调器规则被分成用于控制器和适配对象的规则。控制器（Ctl类）具有与协调器相同的策略和事件属性此外，它还有一个pend属性，表示协调器配置的挂起事件在任何给定时间，一些未决事件可能仍在传输中，即，在包含控制对象的配置此外，还有一个wait4属性，用于在继续之前等待对传输的挂起事件的确认控制器仅在消息可传递时发送rl[ctl.snd]：[c：控制|pend：M m，events：ed，policy：P，wait4：none|输入，输出]=>[c：控制|pend：M，events：ed，policy：P，wait4：m| 输入Q，输出Q m] 如果ed，M，m| = P当收到一个挂起事件的确认时，它包含了消息传递时对象的本地时间，控制器将相应的事件添加到它的事件图属性中。rl[ctl.ack]：[c：控制|pend：M，events：ed，policy：P，wait4：m| （c-ack<（m，j）inQ，outQ]=>[c：控制|pend：M，events：ed e，policy：P，wait4：none|输入，输出]if（a-mb，b，i）：=m/\e：=（mb，a，j，b，i）控制器接收到的挂起事件被添加到其挂起事件中集rl[ctl.rcv]：[c：控制|pend：M，events：ed，policy：P，wait4：w|（c-snd<（m））inQ，outQ]=>[c：控制|pend：M m，events：ed，policy：P，wait4：w|输入，输出]基本对象通过将它们包装在具有相同标识符的定制器具体来说，协调对象定制器有一个包含单个注释对象的配置属性，以及一个值为控制器标识符的属性ctl定制器规则[cust.in]和控制器规则[ctl.snd]154C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）143C{S}区0K我和[ctl.ack]实现协调器规则coord.in。 由于控制器只在消息可传递时发送挂起事件，因此定制器将消息放入对象输入队列，并确认接收，同时添加本地传递时间。rl[cust.in]：[a：CA |{[a：A |atts |nil，nil，j，ready]}，ctl：c| （a<-mb：b，i）inQ，outQ]=>[a：CA| {[a：A|atts|a<-mb，nil，s j，busy]}，ctl：c|inQ，outQ c<-ack（（a<-mb：b，i），j）]定 制 器 规 则 [cust.out] 与 控 制 器 规 则 [ctl.rcv] 一 起实 现 协 调 器 规 则[coord.out]。rl[cust. out]：[a：CA |{[a：A |atts |nil，mQ，j，busy]}，ctl：c|输入，输出]=>[a：CA |{[a：A |atts |nil，nil，j+k，ready]}，ctl：c| inQ，outQ outQ ']如果k：= length（mQ）/|outQ其中mkSnd（mQ，j，c）是消息c-snd（b-mb：a，j+i）的集合，使得b-mb是mQ的第i个元素，从0开始计数因此，由协调器规则[coord.out]生成的挂起事件被打包并发送到控制器。事实上，我们还没有完全消除嵌套，但是定制的对象可以通过简单的模块转换来处理[10]。向定制对象加控制器的转换也是分布对象系统的一种方式，但单个控制器可能不是最合适的解决方案。可以使用类似于基于协调器的系统的分布的定位技术来分布基于协调器的系统。或者，从基于协调器到基于调度器的改进可以适用于改进基于分布式协调器的系统。因此，我们有一个形式为−−→C0{S0}. . . Ck{Sk}↓b↓ b...↓b（CtlS†）−d−i→st（C tl0S†）. . . （CtlkS†其中Ci是第i个分布式协调器，管理子系统Si、Ctli是correspondingconntroller，S†是带注释的定制版本的i。）C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）1431556相关工作有许多语言用于指定或编程协调，其语义已通过各种技术进行了研究。本文提出的工作方法是从分布式对象协调的语义模型开始，重点关注交互而不是系统状态，并研究在一般形式逻辑中指定的语言独立协调机制。对象行为和协调机制是单独指定的，组合操作可以在同一个框架中进行研究元组空间语言包括Linda [13]及其移动扩展Lime [23]。这些语言依赖于（概念上）全局共享数据空间来实现协调，而RRD方法依赖于具有全局视点的协调器具有协调抽象的Actor语言包括同步器[12，11]和实时同步器[24]。这些语言提供了用于指定协调的语言构造，并提供了用于根据标准参与者实现的编译转换它们在精神上接近于基于策略的协调，并且可以通过映射到协调器来直接定义它们的语义。然后，通过细化到基于分布式控制器的规范，可以使编译变得更简单。Reo [4，3]是一种基于通道的协调模型，其中称为连接器的复杂协调器通过组合较小的协调器来构建。文献[2]给出了一个基于时间数据流和共归纳推理原理的语义模型。Klaim[21]是一种基于进程代数的语言。在[22]中，提出了一种方法来设计软件代理之间的代理之间的协调。该方法从需求开始，并通过几个阶段进行细化。在这里，协调被视为代理之间的依赖性，而不是事件的顺序。该方法有相关的图形符号，但缺乏正式的语义。Mobile Unity语言提供了协调原语以及用于推理Mobile Unity规范的逻辑。从高级逻辑规范到移动统一代码的改进在[25]中说明。协调属性基于系统状态而不是交互事件。WS-Coordination规范[16]描述了一个可扩展的框架，用于提供协调分布式应用程序操作的协议。它侧重于初始化、注册和安全等问题156C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）1437未来方向我们已经定义了一个简单的概念的协调需求的基础上的事件图语义的对象系统和可执行规范的基于策略的协调器。通过简单的例子说明了这些想法，并概述了转换为分布式协调器和基层控制器的想法。未来工作的一个明显方向是开发细化规则，以保证对不同类别的策略保持需求满足。需要解决的问题包括：是否有用于推导分布式协调协议的一般原则为组通信的情况所勾画的局部化变换能被推广吗？另一个有趣的方向是考虑协调需求或协调器的组成的概念。容器元对象的组合有几个概念可以探讨。此外，基于策略组合的组合是另一种可能性。在这里，我们可以考虑与协调之外的策略（例如安全）的组合。最后，涉及明确的时间或资源使用的协调是有意义的。为此，语义模型将需要适当地扩展引用[1] G.啊哈Actor：分布式系统中的并发计算模型。麻省理工学院出版社，马萨诸塞州剑桥，1986年。[2] F. Arbab和J.J.M. M.拉顿分量连接符的共归纳演算。技术报告SEN=R0216，Centrum voorWiskunde en Informatica（CWI），2002年。[3] 法哈德·阿巴布一种基于通道的构件组装协调模型。 技术报告SEN=R0203，Centrum voorWiskunde en Informatica（CWI），2002年。[4] F. Arbib. 2001年，移动部件协调[5] 显利贝克和卡尔·休伊特。通信并行进程的法则。 见IFIP Congress，第987-992页。IFIP，1977年8月。[6] Gregory V. Chockler，Idit Keidar，and Roman Vitenberg. 集团通信规范：一项全面的研究。ACM Computing Surveys，33（4）：1[7] M. Clavel，F. 杜兰，S。 Eker，P. 林科林，N。 妈的，J. Meseg u er，andC. Talcottt. 马乌德2.0手册，2003年。 http://maude.cs.uiuc.edu。[8] M. Clavel，F. 杜兰，S。 Eker，P.Lincoln，N. 我的天啊-我的天啊。 我是你，还有C。 L.Talcott. Maude 2.0 系 统 在 Robert Nieuwenhuis ， 编 辑 ， Rewriting Techniques andApplications（RTA 2003），计算机科学讲义第2706卷，第76Springer-Verlag，2003.[9] W. D.粘人演员语义学的基础。AI-TR- 633，MIT人工智能实验室，1981年5月。C.L. Talcott/Electronic Notes in Theoretical Computer Science 150（2006）143157[10] G. Denker，J. Meseguer，and C. L.塔尔科特 分布式Meta对象和可组合通信服务的重写语义。在第三届重写逻辑及其应用国际研讨会爱思唯尔，2000年。[11] S.弗伦德协调的分布式对象：一种基于参与者的同步。MIT Press，1996.[12] S. Frølund和G.啊哈一种多对象协调的语言框架。 在ECOOP 1993年，计算机科学讲义第707卷。Springer，1993年。[13] 大卫·格勒恩特。 琳达的生成通信。 TOPLAS，7（1）：80[14] I.格雷夫通信并行进程的语义。技术报告154，麻省理工学院，MAC项目，1975年。[15] C. Hewitt ， P. Bishop ， and R. 史 泰 格 A Universal Modular Actor Formalism for ArtificialIntelligence（人工智能的通用模块化行动者形式主义）1973年国际人工情报联合会议论文集，第235-245页，1973年8月[16] IBM、Microsoft和IBM Systems。 Web服务协调，2004年。[17] Narciso Marti-Oliet，Jose Meseguer，and Miguel Palomino.重写逻辑与应用参考书目。理论计算机科学，285（2），2002年。[18] J. Meseguer。条件重写逻辑是并发的统一模型。Theoretical Computer Science，96（1）：73[19] J. Meseguer和C. L.塔尔科特分布式对象反射的语义模型。在欧洲面向对象编程会议，ECOOP邀请函[20] 乔 是 我 的 老 师 。 Rewr ritinglgicnmAde-spectmanticframew r a m eronect-based distributedsystems.In S.史密斯和C.L. Talcott，编辑，开放式基于对象的分布式系统的形式化方法，FMOODS 2000，第89-117页。Kluwer，2000年。[21] R. De Nicola，G. Ferrari和R.普利亚人 KLAIM：一种用于代理交互和移动性的内核语言。IEEE软件工程学报，24（5）：315[22] 安娜·佩里尼，安杰洛·苏西，福斯托·朱奇利亚。多智能体系统中的协调规范：从需求到架构与Tropos方法。第14届软件工程和知识工程国际会议，第51-54页。ACM Press，2002.[23] G. 皮 科 角 墨 菲 和 G.- C. 罗 曼 LIME ： Linda 符 合 流 动 性 。 在 21 Int. Conf. on SoftwareEngineering，第368-377页[24] 上坪。仁一个基于角色的实时协调框架。博士论文，伊利诺伊大学香槟分校，1997年。[25] Gruia-Catalin Roman，Christine Julien，and青峰Huang.移动系统的形式规范和设计。并行编程的形式化方法：理论与应用，2002年。[26] C. L.塔尔科特行动者理论的可组合语义模型。高阶和符号计算，11（3）：281
