Mobile Maude: 一种分布式移动代理的规范/实现

理论计算机科学电子笔记176（2007）113-131www.elsevier.com/locate/entcsMobile Maude*的分布式实现FranciscoDura'n，aAdria'nRiesco，b和Alb ertoVerdejobaETSIInform'ati ca，UniversidaddeMa'laga，Spain. duran@lcc.uma.esb西班牙马德里孔普卢顿大学信息学硕士。ariesco@fdi.ucm.esalberto@sip.ucm.es摘要我们提出了一个新的规范/实现的移动代理语言Mobile Maude。这个新版本使用了Maude自2.2版本以来提供的外部套接字，从而获得了移动语言的真正分布式实现，其中消息和移动对象现在可以以透明的方式从一台机器传输我们还展示了如何，即使移动Maude规范的复杂性和反射的使用，我们已经设法使用Maude保留字：移动代理，Mobile Maude，模型检查。1介绍Mobile Maude是对Maude语言的扩展，支持移动计算的移动Agent语言[ 3 ]第一次出现在[4]中，并在[4]中出现了重要的应用。Mobile Maude使用反射来获得一个简单而通用的声明式移动语言设计，并使移动代理行为的强保证成为可能。利用重写逻辑中的重写理论给出了Mobile Maude的形式语义。由于此规范是可执行的，因此可以将其用作语言的原型，在其中可以模拟移动代理系统。两个关键概念是过程和移动对象。进程位于移动对象可以驻留的计算环境中。移动对象有自己的代码，可以在不同位置的不同进程之间移动，并且可以通过消息彼此异步通信。Mobile Maude研究部分得到MCyT西班牙项目MIDAS（TIC 2003-01000）和TIN 2005 - 09405-C 02 -01的支持。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.011114F. Durán等人理论计算机科学电子笔记176（2007）113作为一种赋予移动对象“高阶”能力的方式的反射移动对象的代码由基于对象的模块（的元表示）给出-重写理论-其数据由表示其状态的对象和消息的配置给出。这样的配置在代码模块中是一个有效的术语，用于执行它。Maude配置成为移动对象可以驻留的定位计算环境。移动对象可以与其他对象交互（可能在不同的位置），并且可以从一个位置移动到另一个位置。在[3]中，Dura'n、E ker、Lincoln和Meseguer首次介绍了MobileMaude。在这项工作中，作者提出了一个Mobile Maude的“模拟器”，一个可执行的Maude规范，在Maude 1.0.5之上，其中系统代码完全用Maude编写，因此位置和进程被编码为Maude术语。 在同一篇论文中，作者还给出了一个开发计划，包括两个开发步骤：第一步是实现单主机可执行文件，第二步是专注于真正的分布式执行。Maude 2.0的发布允许迈出第一步。 这个实现排序是在很短的时间内完成的，利用内置的对象系统，为了对象/消息的公平性，只是通过简化和扩展以前的规范。这一新版本是由Duran′n和Verdejo提出的，并用于几个实例中，其中一个在[4]中报道本文总结了二次开发的结果。Maude 2.2中内置的字符串处理和互联网套接字模块允许我们构建一个真正的分布式实现。Maude 2.2套接字模块支持非阻塞客户端和服务器TCP套接字（在操作系统级别）。在这种实现方式中，Mobile Maude服务器运行在Maude解释器之上，并执行以下任务：跟踪在主机上创建的移动对象的当前位置，处理位置消息的更改，将消息重新路由到移动对象，并通过调用元级来运行移动对象的代码。事实上，我们已经在Mobile Maude上进行了大量的更改。进程和位置不再是Mobile Maude规范的一部分，现在我们讨论的是Maude进程（不是术语，而是可能在不同机器上运行的OS进程）和IP地址。 我们还引入了根对象的概念，作为不同进程中移动对象配置的管理器。我们将在下面解释进程和移动对象的设计以及它们的重写语义，基于用Maude编写的Mobile Maude的正式规范Mobile Maude的基本概念，即进程、移动对象和消息将在第2节中介绍。在第三节中，我们对Mobile Maude的重写语义进行了分析。在第4节中，我们讨论了分布式配置中不同进程之间通过套接字的连接;特别是，我们介绍了Maude套接字，我们解释了缓冲套接字，然后介绍了一个非常简单的示例架构。第5节介绍了MobileMaude应用程序代码F. Durán等人理论计算机科学电子笔记176（2007）113115o（1（IP，0），1）o（1（IP，0），1）I（IP'，0）o（1（IP，0），0）o（1（IP '，0），0）l（IP，0）Fig. 1. 对象和消息移动性。在这个例子中，我们指定了在几个分布式备选方案之间搜索最佳备选方案。第6节解释了我们如何使用模型检查器来检查Mobile Maude规范的属性。第7节用一些最终结论来包装这部作品。2进程、移动对象和消息Mobile Maude中的关键实体是进程和移动对象。移动对象在MobileObject类中被建模为分布式对象。分布式配置由定位配置组成每个定位配置都在Maude过程中执行。因此，这样的进程可以被看作是位于计算环境中的移动对象可以驻留、执行以及向位于不同进程中的其他移动对象发送消息和从位于不同进程中的其他移动对象接收消息。我们认为，每个定位的配置都有一个（且只有一个）根对象，即RootObject类，它保存有关进程位置的信息，有关这种配置中的移动对象的信息，以及有关其中创建的移动对象的位置的信息，这些移动对象可能已经移动到其他进程。我们假设在分布式配置中根对象名称的唯一性移动对象携带自己的内部状态和代码（重写规则），可以从一个进程移动到另一个进程，并且可以通过异步消息传递相互通信。根对象的名称范围在排序Loc上，并且具有l（IP，N）的形式，其中IP是正在执行进程的机器的IP地址，N是数字。移动对象的名称范围在排序Mid上，形式为o（L，N），其中L是创建它的进程的根对象的名称，N是一个数字。图1示出了两个进程中的若干移动对象，其中（移动）对象o（1（IP，0），1） 从具有根对象1（IP，0）的进程移动到根对象1（IP ′，0）的进程，并且对象o（1（IP，0），0）向o（1（IP ′，0），0）发送消息。移动对象被指定为以下类MobileObject的对象：11我们在这里使用Full Maude面向对象表示法来定义类。然而，Mobile Maude的实际实现是在Core Maude中实现的，因为Full Maude不支持外部对象。的116F. Durán等人理论计算机科学电子笔记176（2007）113MobileObject类|mod： Module，* 重写移动对象的规则s：术语，***当前状态天然气：天然气，* 受资源跳数：Nat，* 跳数mode：模式。* 运 动 中 的 物体不能处于活动状态排序Module和Term分别与属性mod和s相关联，是模块META-LEVEL中的排序。移动对象&在对象和消息的配置中，其中一个对象应该与它所在的移动对象具有相同的标识符。 我们有时把这个对象称为主要对象，在大多数情况下，它将是唯一的对象。因此，我们可以将移动对象看作是一个包装器，它封装了其内部对象的状态和代码，并调解了它与其他对象的通信及其移动性。出于这个原因，图1用两个同心圆来描述移动对象，内部对象及其传入和传出的消息包含在内部圆中。为了保持转发信息是最新的（见下文），类MobileObject的定义包括属性hops，它存储从一个进程到另一个进程的“跳”数 为了保证所有移动对象最终都有一些活动，并且作为它们可以消耗的资源的限制，它们具有gas属性。最后，对象的模式只在进程内部活动：在途对象是空闲的。根对象的类RootObject声明如下：类RootObject|cnt： Nat，* 生成移动对象的计数器。名称guests：设置{Oid}，位置中的 * 对象forward：Map{Nat，Tuple{Loc，Nat}}，* 转发信息状态：RootObjectState，* 空闲、等待连接或活动邻居：Map{Loc，Oid}，* 将套接字关联到每个位置defNeighbor：Default{Oid}。* 默认套接字我们假设每个定位的配置包含一个且只有一个根对象，加上当前驻留在这样一个进程中的消息和移动对象。运行在不同Maude进程上的定位配置构成了分布式配置。移动对象可以从一个进程（定位配置）移动到另一个进程。每个进程的根对象在guests属性中保存有关当前进程中移动对象的信息。移动对象用形式为o（L，N）的标识符命名。属性cnt存储一个计数器，用于生成这种唯一的新移动对象名称。由于移动对象可以从一个进程移动到另一个进程，因此通过消息到达它们是不平凡的。 Mobile Maude [3]中采用的解决方案是，当消息的收件人不在当前进程中时每个Mobile Maude的完整代码，包括Core Maude中相应的类声明MobileObject和RootObject可以在www.example.com中找到http://maude.sip.ucm.es/mobilemaude。F. Durán等人理论计算机科学电子笔记176（2007）113117根对象在其forward属性中存储关于其子进程的位置的转发信息，该属性是Map{Nat，Tuple{Loc，Nat}}中的部分函数，该函数将子进程编号n映射到由对象当前所在的已定位进程的名称和移动对象到目前为止所采取的不同进程的“跳”数当旧消息（包含旧位置信息）在包含当前位置的新消息之后到达时，跳数在消除歧义的情况最新位置是与最大跳数相关联的位置。每当一个移动对象移动到一个新进程时，该对象的父进程总是会被通知。请注意，在对象比消息移动得更快的情况下，此机制不能保证消息传递在Mobile Maude的前一个版本中，所有进程都在相同的Maude面向对象配置中，并且到达特定进程由一个规则表示然而，在这个新版本中，当一个移动对象移动到不同的位置，或者一个消息被发送到不同位置的移动对象时，由于我们使用TCP套接字来连接进程，我们需要知道哪个套接字必须用来发送信息。进程中的根对象负责通过适当的套接字发送它2.假设所有进程都直接相互连接是不现实的，我们可以连接的进程数量非常有限，并且连接新进程的任务非常昂贵。幸运的是，两个节点之间的连接并不一定意味着它们之间的直接连接。可以在一组协作节点之间实现间接连接。然而，仅仅因为一组主机直接或间接地相互连接并不意味着我们已经成功地提供了主机到主机的连接。当源节点希望网络将消息传递到某个目的节点时，它指定目的节点的地址。 如果发送节点和接收节点没有直接连接，那么它们之间的网络节点（交换机和路由器）使用此地址来决定如何将消息转发到目的地。系统地确定如何根据目的节点的地址将消息转发到目的节点的过程（通常称为路由）是非常重要的。3在这里，我们假设一个非常简单，但相当普遍的方法，包括在每个根对象中有一个路由表。这样一个表给出了一个套接字，如果一个人想要到达一个特定的位置，消息必须通过这个套接字发送。 如果消息的源和目标之间存在套接字，那么它可以在一个步骤中到达目的地;否则转发必须重复多次。neighbors属性维护这样一个路由表，作为将套接字对象标识符与位置标识符相关联的映射也就是说，属性neighbors在部分函数Map{Loc，Oid}中存储有关套接字的信息，通过套接字发送数据以到达特定位置。2正如我们将在接下来的章节中看到的，根对象通过缓冲套接字发送消息。我们将在第四节讨论插座和带插座的使用。3我们只考虑源节点想要向单个目的地节点发送消息（单播）的情况。多播的情况-源节点想要发送消息到网络上的节点和广播源节点想要向网络上的所有节点发送消息可以类似地被指定。118F. Durán等人理论计算机科学电子笔记176（2007）113如果在地图邻居中没有与特定位置相关联的套接字，则可以在属性defNeighbor中存储默认套接字。然而，defNeighbor属性的值也可以不指定。在下面的模块DEFAULT-ELEMENT中声明的排序Default{X}向模块实例化中使用的排序添加了一个默认值。我们定义了参数化的函数模块DEFAULT-ELEMENT{X：：TRIV}，其中我们声明了一个排序Default{X}作为参数理论的排序Elt的超排序，以及一个排序Default{X}的常量null。fmod默认元素{X：： TRIV}是排序默认值{X}。子排序X$Elt<默认值{X}。opnull：-> Default{X}[ctor].endfm然后，由于defNeighbor被声明为Default{Oid}排序，因此它可以将对象标识符或null作为值。如果没有与特定位置关联的套接字，而默认套接字有如果没有指定，则数据不会被传递。请注意，这个模型允许我们表示许多不同的网络架构，尽管我们在这里不关心它，但路由信息可以以非常灵活的方式更新和使用。 我们将在4.2节中解释如何构建一个非常简单的架构。最后，根对象可能处于空闲、等待连接或活动状态。属性state将采用这些值之一。根对象只有在创建时才是空闲的，这是它们作为客户端或服务器套接字激活的第一个动作它们一直处于等待连接状态，直到从服务器套接字得到确认，然后进入活动模式，在这种状态下，它们将开展正常的活动。Mobile Maude系统代码由根对象、移动对象、移动性和消息传递的相对较少的规则（大约40条）指定。 这些规则以独立于应用程序的方式工作。另一方面，应用程序代码可以被编写为具有很大自由度的Maude基于对象的模块，除了意识到，如上所述，移动对象的状态的顶层必须是 一对配置，第二个组件包含传出消息，第一个组件包含内部对象和传入消息。对MobObjState进行排序。op_&_：Configuration-> MobObjState [ctor].被拉入或拉出移动对象的消息必须是O：C，go（L），go-find（O，L），newo（Mod，Conf，O）或kill的形式，其中L是位置（Loc类），O是 移 动 对 象 标 识 符 （ Mid 类 ） ， C 是 内 容 （ Contents ） ， Mod 是 模 块（Module），Conf是配置（Configuration）。这样的消息实际上可以被理解为在移动对象的内部配置中的对象或对象之一给予它的命令。因此，对象可以向对象O发送具有内容C的消息，其中消息为toO：C;可以请求从其当前位置移动到给定位置L，其中消息为go（L）;可以请求前往移动对象O所驻留的位置，其可能是L，其中消息为go-find（O，L）;可以请求创建具有模块Mod、初始状态Conf和在这样的配置中的主对象的时间标识符的新移动对象。F. Durán等人理论计算机科学电子笔记176（2007）113119configurationO，消息newo（Mod，Conf，O）;或者可以请求破坏它驻留的移动对 象 ， 消 息 kill 。 所 有 这 些 成 分 的 定 义 都 在 模 块 MOBILE-OBJECTIVE-ADDITIONAL-DEFS中定义，该模块假定由用户在其所有Mobile Maude应用程序中导入。注意，发送到其他移动对象的消息必须是to_：_的形式，消息的收件人作为第一个参数，排序内容作为第二个参数。这种类型的定义留给每一个特定的应用程序（见第5节），实际上让用户自由定义任何类型的消息，限制是将收件人的标识符作为第一个参数。3Mobile MaudeMobile Maude的整个语义可以用一个相对较小的数字来定义用Maude重写规则。我们应该将这些规则视为Mobile Maude系统代码的实现/规范，它以独立于应用程序的方式运行，提供所有对象创建和销毁、消息传递和对象移动原语。通过对Mobile Maude重写语义的一些规则的评论，对Mobile Maude重写语义进行了分析。特别地，我们关注负责传递对象间消息的规则，因为除了说明一般方法（更详细的讨论可以在[3]和[4]中找到）之外，它直接与新实现中的主要新特性：套接字有关。完整的规范，包括相同风格的其他规则，可以在www.example.com中找到http://maude.sip.ucm.es/mobilemaude。 对象之间有三种通信方式。 同一移动对象内部的对象可以通过任何格式的消息相互通信，并且这种通信可以是同步的或异步的。不同移动对象中的对象可以在这些移动对象处于同一进程和处于不同进程时进行通信;在这些情况下，实际的通信类型对移动对象是透明的，但这种通信必须是异步的，通过形式为_：_的消息，如上所述如果收件人是不同移动对象中的对象，则必须将消息由发送者对象在其状态的第二个组件（传出消息托盘）中执行。 然后系统代码将消息发送到收件人对象。 第一消息被拉出对象rl [message-out-to]：< O：V@MobileObject|mod：MOD，s：&'_ _[ T ， 'n o n e .C o n f i g u r a t io n ] ， 模式 ： 活 动 ， At S > （ 到 do w nT e r m （ T '， o（ 1（ “ nu l l ” ， 0 ） ， 0 ） ） {T “ } ）。一旦消息离开移动对象，它就可以被适当地传递。下面的msg-send规则将邮件重定向到不同位置的移动对象。crl[msg-send]：（到o（L，N）{T}）=>< L：V@RootObject|状态：活动，访客：OS，转发：F，AtS >发送（p1（F[N]），L，到p1（F[N]）{ T }中的o（L，N）跳p2（F[N]））120F. Durán等人理论计算机科学电子笔记176（2007）113如果（p1（F[N]）= l = L）/l（在OS中不是o（L，N））。注意消息的使用opSend：Oid Oid Msg-> Msg [ctor msg].发送信息到合适的地点 第一和第二个论点Send消息分别是消息的收件人和发件人，第三个参数是正在发送的消息。 我们将在第4节中看到，发送消息将用于通过适当的套接字发送相应的数据。对象间消息到达收件人对象 是，由以下规则处理。消息只是放在位置上，这样对象就可以得到它。rl [msg-arrive-to-loc]：到L' { T' }中的o（L，N）跳 H< L '：V@RootObject|状态：活动，访客：（o（L，N），OS），AtS>=>到o（L，N）{T' }。一旦消息到达它的收件人对象，消息必须插入-推入-这样一个移动对象的状态。为了确保移动对象将保持在有效状态，我们检查相应消息的元表示是否是对象模块中的有效消息rl[msg-in]：到O{T}< O：V@ MobileObject|模：模D，s：&'_ _[T'，T '']，AtS>=>ifsortLeq（MOD，leastSort（MOD，或者sortLeq（MOD，<'Msg，leastSort（MOD，'to_：_[upTerm（O），T]））then O：V@ MobileObject|mod：MOD，s：&<' _ _ [''to_：_ [upTerm（O），T]，T']，T'']，AtS > else O：V@MobileObject|mod：MOD，s：&'_ _[T'，T'']，AtS>菲4套接字处理Maude 2.2支持使用外部对象重写，并将sock- ets实现为第一个外部对象。 使用外部对象重写是由命令ererwrite（缩写为erew）启动的，它类似于frewrite，但它允许与不驻留在配置中的外部对象交换消息。套接字是使用模块SOCKET中声明的消息访问的，可以在Maude分发的socket.maude文件我们在这里简单描述Maude插座。对于Maude套接字的完整解释，它们的使用和示例，我们建议读者参考Maude手册[2]。目前仅支持IPv4TCP套接字;将来可能会添加其他协议系列和套接字类型由常量socketManager命名的外部对象是套接字对象的工厂。要创建客户端套接字，必须向socketManager发送一条消息“ClientTcpSocket（socketManager，ME，ADDRESS，PORT）”，其中ME是应答应发送到的对象的名称ADDRESS是要连接的服务器的名称，PORT是要连接的端口F. Durán等人理论计算机科学电子笔记176（2007）113121(say 80用于HTTP连接）。回复将是消息createdSocket（ME，socketManager，SOCKET-NAME），其中SOCKET-NAME是新创建的套接字的名称客户端套接字上的所有错误都通过关闭套接字来处理然后，您可以使用消息send（SOCKET-NAME，ME，DATA）将数据发送到服务器，该消息sent（ME，SOCKET-NAME）将删除已发送的消息。类似地，您可以使用消息receive（SOCKET-NAME，ME）从服务器接收数据，该消息删除了消息received（ME，SOCKET-NAME，DATA）。要在两个Maude解释器实例之间进行通信，其中一个必须承担服务器角色，并在给定端口上运行服务。要创建服务器套接字，请向socketManager发送一条消息SocketServerTcpSocket（socketManager，我，港口，海港）其中，PORT是端口号，REQ是您将允许的队列连接请求数。回应就是信息createdSocket（ME，socketManager，SERVER-SOCKET-NAME）.这里SERVER-SOCKET-NAME指的是服务器套接字。对于服务器套接字，您唯一能做的就是通过消息接受客户端acceptClient（SERVER-SOCKET-NAME，ME）这就解释了acceptedClient（ME，SERVER-SOCKET-NAME，ADDRESS，NEW-SOCKET-NAME）.这里ADDRESS是客户端的源地址，NEW-SOCKET-NAME是用于与客户端通信的套接字的名称。这个新套接字的行为就像一个发送和接收的客户端套接字正如我们在第3节中所看到的，Mobile Maude的规范不知道套接字。我们唯一接近套接字的地方是在使用发送消息时，这实际上不是套接字消息，而是一个缓冲套接字消息。我们在4.1节中介绍了buffered sockets，一种过滤器类，它使MobileMaude独立于sockets，同时它增加了一些额外的功能。 作为我们将在第6节中看到，正是这种独立性使我们能够以一种相当干净的方式对Mobile Maude规范进行模型检查。 第4.2节谈论系统的架构，流程如何连接，并展示如何 做一个非常简单的建筑。4.1布氏插座TCP套接字不保留消息边界。因此，发送例如消息“ONE”和“TWO”可能导致消息“ON”和“ETWO”的接收。虽然在其他应用程序中不相关，但在当前情况下，我们需要保证消息按照最初发送的方式接收;例如，如果通过套接字发送移动对象，则我们需要能够恢复有效对象，在收到消息后，它被发送的有效状态。为了保证消息边界，我们使用了一个过滤器类BufferedSocket，在模块BUFFERED-SOCKET中定义。该模块完全独立于Mobile Maude，因此可以用于其他应用程序。我们与被包围的插座互动，122F. Durán等人理论计算机科学电子笔记176（2007）113与我们与套接字交互的方式相同，唯一的区别是SOCKET模块中的所有消息都被大写以避免混淆，边界控制对用户完全透明当创建BufferedSocket时，除了发送信息的Socket对象之外，还在Socket的每一端创建BufferedSocket对象（在建立通信的每一个配置所有通过缓冲套接字发送的消息在通过下面的套接字发送之前都要经过处理当消息通过缓冲套接字发送时，在消息的末尾放置一个标记;套接字另一端的BufferedSocket对象存储缓冲套接字上接收到的所有消息，当请求消息时，放置的标记表示接收到的信息的哪一部分必须作为下一条消息给出一个BufferedSocket类的对象有三个属性：read，sort String，它存储读取的消息，bState，它指示过滤器是空闲的还是活动的，以及waiting，它指示我们是否在等待发送的消息（当我们在等待时，我们不允许发送新消息）。对BState排序。ops idle active：-> BState [ctor].类BufferedSocket|read：String，bState：BState，waiting：Bool.我们在这里没有给出所有的规则，而只是那些与发送消息有关的规则。一旦建立了连接，并且在每一端都创建了BufferedSocket对象，就可以发送和接收消息了。 当接收到一个发送消息时，缓冲套接字发送一个发送消息，该消息具有相同的数据加上一个标记4以指示消息的结束rl[send]：Send（b（SOCKET），O，DATA）=>send（SOCKET，O，DATA+“#”）.关键在于接收信息。BufferedSocket对象始终侦听套接字。它在启动时发送一个接收消息，并将所有接收到的消息放在它的缓冲器中。请注意，在缓冲区启动规则中，被缓冲的套接字从空闲变为活动。 如果缓冲器中有一个完整的消息，也就是说，上面有一个标记，则接收消息被处理，并导致接收缓冲器中的第一个消息，该消息被从缓冲器中删除rl [buffer-start-up]：=> receive（SOCKET，b（SOCKET））.rl[接收]： received（b（SOCKET），O，DATA）=>receive（SOCKET，b（SOCKET））.crl[接收]：4在规则中，我们使用字符串“#”作为标记，但可以使用任何其他标记。请注意，通过套接字发送的用户数据不应包含此类标记。F. Durán等人理论计算机科学电子笔记176（2007）113123 Receive. bState（b（SOCKET），O）=>< b（SOCKET）：V@BufferedSocket |bState：active，read：S'，Atts > Received（O，b（SOCKET），DATA）ifN：= find（S，“#"，0）/\DATA：= substr（S，0，N）/\S '：= substr（S，N + 1，length（S））.4.2客户端/服务器架构虽然在前面的章节中介绍的Mobile Maude的规范允许不同的进程配置，但我们在这里介绍一个非常简单的客户端/服务器架构。我们通过声明RootObject的两个子类ServerRootObject和ClientRootObject来区分客户端和服务器，没有额外的属性，尽管具有不同的行为。类ClientRootObject。类ServerRootObject。子类ClientRootObject ServerRootObject 接受客户端（I（IP，N），套接字，IP '，新套接字）=>AcceptClient（SOCKET，I（IP，N））接收（新套接字，l（IP，N））Send（NEW-SOCKET，l（IP，N），msg2string（new-socket（l（IP，N）.由于Send消息的第三个参数是String，因此发送的消息将使用msg 2string函数进行转换;string 2 msg执行逆转换。对客户端根对象的套接字连接请求的响应由下面的规则连接，其中客户端也在套接字创建后立即发送新套接字rl[已连接]：CreatedSocket（O，SOCKET-BASHER，SOCKET）124F. Durán等人理论计算机科学电子笔记176（2007）113=>ReceiveN（SOCKET，I（IP，N））Send（SOCKET，l（IP，N），msg2string（new-socket（l（IP，N）.属性neighbors和defNeighbor是通过适当的套接字发送消息的关键。创建套接字后通过套接字发送的第一个消息是消息new-socket的原因是初始化这些属性。当它被接收时，取决于接收者是客户端还是服务器，以及是否已经存在默认邻居，采取一个或另一个动作为了避免在消息传递过程中出现意外循环，我们假设服务器根对象没有默认邻居。对于客户端，第一个连接是默认连接。crl[接收]：< O：V@RootObject|状态：活动，邻居：空，defNeighbor：null，AtS> Received（O，SOCKET，DATA）=>< O：V@ root对象|状态：活动，邻居：插入（L，SOCKET，空），defNeighbor：如果 V@RootObject ==ServerRootObject，则为null否则套接字fi，AtS>接收（SOCKET，O）if new-socket（L）：= string2msg（DATA）.crl[接收]：接收（O，套接字，数据）=>< O：V@ root对象|状态：活动，neighbors： insert（L，SOCKET，LSPF），AtS>接收（SOCKET，O）if LSPF=/= empty/\new-socket（L）：= string2msg（DATA）.如果不是一个新套接字消息，那么消息就留在配置中crl[接收]：Received（O，SOCKET，DATA）=> string 2 msg（DATA）接收（SOCKET，O）如果不是新套接字（DATA）。5购买打印机的例子在本节中，我们将展示一个简单的应用程序，以说明如何用Maude编写移动应用程序代码，以及如何将其包装在移动对象中。 在这个例子中，我们有打印机、买家和卖家;一个买家代理访问几个打印机卖家，这些卖家向他提供有关打印机的信息。买家寻找最便宜的打印机，一旦他访问了所有的卖家，他回到卖家的位置，以获得最好的价格。从前面的描述中，我们可以识别不同的参与者，他们可以自由地从一个过程移动到另一个过程，因此他们应该被表示为移动对象。在Mobile Maude方法中，系统的规范由嵌入在移动对象中的对象组成，这些对象通过消息相互通信。除了表示其状态的术语之外，每个移动对象还携带管理对象配置行为的代码和表示这种状态的消息。在Maude中，关于系统规范的主要区别在于，这些对象必须意识到它们是F. Durán等人理论计算机科学电子笔记176（2007）113125在移动对象内部，为了与其他移动对象（对象）通信或使用某些可用的系统消息，它们必须遵循 适当的程序。在我们的示例应用程序中，我们有两类不同的移动对象：卖家和买家。 一个买家拜访了几个卖家。 买家向他拜访的每一个卖家询问 卖方打印机的描述（此处仅以其价格表示）。卖方发送回这些信息，如果它对应于更好（更便宜）的打印机，买方将保留这些信息。一旦买家拜访了他认识的所有卖家，他就会回到最好的卖家那里我们代表卖方和买方作为各自类别卖方和买方的对象。 应用程序代码中的此类对象将作为内部对象嵌入对应的移动物体。类Seller具有打印机价格（自然数）的单个属性描述类别卖方|描述：Nat.卖方接收get-printer-price（B）形式的消息，其中B是发送消息的买方移动对象的标识符。卖方可以发送形式printer-price（N）的消息，其中N是代表打印 机 价 格 的 自 然 数 两 者 都 定 义 为 sortContents， 在 模 块 MOBILE-OBSERVED-ADDITIONAL-DEFS中声明。op get-printer-price：Mid-> Contents.op printer-price：Nat -> Contents.卖方的行为由以下单个重写规则表示：当卖方收到描述（价格）请求时，它将描述发送回买方。rl[get-des]：(toS：获取打印机价格（B））无&配置=>< S：V@卖家|Description：N，AtS >Conf&（toB：printer-price（N））.注意__构造函数的使用。由于打印机描述被发送到卖方对象所在的移动对象之外的对象，因此消息放在右边。get-des规则仅在传出消息托盘为空时应用，以这种方式确保任何先前的传出消息都已被处理。 __运算符是表示移动对象的状态，因此，由于在其左侧的配置中可能有其他对象和消息，因此我们包含一个排序为Configuration的变量Conf来匹配其余部分。