127理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html17页Mobile Maude会议评审系统FranciscoDura'na，1和 AlbertoV erdejob，2aETSIInforma'ti ca，马拉加大学，西班牙。bFacultaddeInforma′ti ca，西班牙马德里孔普鲁腾塞大学。摘要介绍一种新语言的一个有用的方法是通过完整的例子来展示语言的功能。 在本文中，我们这样做的移动Maude语言，扩展Maude支持移动计算。我们实现了一个雄心勃勃的广域应用程序，即会议审查系统，一个例子描述的Cardelli作为一个挑战，任何广域语言，以证明其可用性。关键词：广域语言，移动计算，移动代理，移动Maude1引言Internet的普及给分布式应用程序开发带来了极大的关注。现在，网络比以往任何时候都更被视为开发成本效益高、任务关键型应用程序的平台。移动代码和移动代理[12，11]是新兴的技术，有望使分布式系统的设计，实现和维护变得更加容易。移动代理可以减少网络传输，提供一种有效的手段，克服网络延迟，也许更重要的是，帮助我们构建更强大的和容错的系统，由于他们的异步操作和自主的过程，创建它们的能力。虽然分布式应用程序代表了一个巨大的潜在的未来，编写分布式应用程序运行在互联网上的任务是与可扩展性，可靠性和安全性的问题。现在的应用规模*由项目TIC 2000 -0701-C 02 -01和TIC 2001 -2705-C 03 -02资助的研究。1电子邮件地址：duran@lcc.uma.es2电子邮件地址：alberto@sip.ucm.es2003年3月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。杜兰和贝尔德霍128考虑用于网络环境将需要更高级别的安全性和可靠性。为了使代理系统为这些应用提供一个现实的开发替代方案，这些系统必须发展，以提供所需的高度安全和可靠的环境。对于这样的任务，具有精确语义的内在并发形式主义似乎是不可避免的，声明性方法似乎很有前途。重写逻辑对于表示非常不同的通信风格（同步或异步）的灵活性，它对于支持分布式、并发面向对象系统的便利性，以及它对于支持元编程和动态重构的响应能力，使得它一个非常合适的形式主义的规范的分布式系统的基础上移动代理，证明有关的安全性，正确性和性能的属性，可以基于。最近，多范式的扩展，声明性语言Maude[5]已经提出了支持移动计算的机制。它被称为Mobile Maude[7]，它的主要特点使它成为一种适合基于移动代理的分布式系统的规范和原型设计的语言：（1）它基于重写逻辑，这是一种简单的逻辑，易于用于并发，分布式和开放系统的规范，包括数据，事件，系统演化，安全和实时等方面(2) 它是面向对象的，支持分布式对象及其同步或异步通信，具有正式的、精确的语义;(3) 它是响应性的，在任何层次上都对元编程提供了正式的支持;（4）它是广谱的，允许对规范进行转换和细化;（5）它是模块化的，具有高级模块系统;（6）它是移动的，支持数据、状态和程序的移动;（7）它有一个正式的基础来开发安全模型，并验证这些模型的属性。这项工作的目的是促进对Mobile Maude的理解，说明该语言在特定应用程序中的主要特征，即会议的审查系统，从会议的宣布到会议记录的编辑。Cardelli在[2]中提出了这样的例子，作为对任何广域语言证明其可用性的挑战，尽管它以前被不同的作者使用第2节描述了Mobile Maude。第3节包括对会议审查系统的描述，以及对我们的Mobile Maude实现的详细解释。第4节讨论了一些相关的工作。在第五部分，我们提出了一些结论和未来的工作。2莫比尔·莫德莫比尔·莫德（MobileMaude）在[7]中首次描述。 我们在这里对该语言进行了简要的讨论，展示了它的关键概念和下面使用的原语。杜兰和贝尔德霍129路段Mobile Maude是一种移动Agent语言，它扩展了重写逻辑语言Maude以支持移动计算。在其设计中，系统地使用了反射，得到了一种简单而通用的声明式移动代理语言。Mobile Maude已经通过重写理论正式指定。由于该规范是可执行的，因此可以将其用作语言的原型，在该语言中可以模拟移动代理系统。Mobile Maude基于两个关键概念：进程和移动对象。进程位于移动对象可以驻留的计算环境中。移动对象可以在不同的进程之间移动，可以通过消息彼此异步通信，并且可以进化。在Mobile Maude中，移动对象可以与同一进程或不同进程中的对象进行通信-一些移动代理语言禁止后一种通信，只允许进程内的通信。移动对象带着自己的数据和代码移动。移动对象的代码由面向对象模块（的元表示）给出-重写理论，其数据由表示其状态的这样的配置是一个有效的术语，代码模块，用于执行它。进程和移动对象分别被建模为类P和MO中的分布式对象。进程的名称范围在排序Pid上，进程的类P的声明如下。P类|cf：Configuration，cnt：Int，guests：Set（Mid），forward：PFun（Int，Tuple（Pid，Int））。cf属性表示内部配置，移动对象和消息可以驻留在其中。因此，一个移动代理系统将由一个进程配置（以及进程之间的消息转换）组成，每个进程内部都有一个移动对象配置。guests属性保存当前进程内部配置中的移动对象的名称cnt属性是一个计数器，用于生成新的移动对象名称。移动对象的名称范围在排序Mid上，并且它们具有o（PI，N）的形式，其中PI是对象的主进程或父进程的名称PI的孩子们这个数字是由cnt属性提供的，它在创建一个新的移动对象后增加。消息的调度为了解决这个问题，每个进程都在其forward属性中保持转发有关其子进程的位置的信息，forward属性是跳数用于了解保存在父母每次移动对象移动到不同的进程时，它都会向其主进程发送一条消息，通知其新位置。移动对象的类声明如下：杜兰和贝尔德霍130MO类|mod：Module，s：Term，p：Pid，hops：Int，mode：Mode。s属性保存移动对象的状态（的元表示），并且必须&在对象和消息的配置中，其中一个对象应该与它所在的移动对象具有相同的标识符。 我们把这个物体称为主要一。 mod属性是描述对象行为的Maude模块的元表示。 p属性保存对象当前所在进程从一个节点到另一个节点的跳数由对象执行的到另一个对象的过程存储在hops属性中。最后，如果对象在进程内，则对象Mobile Maude的语义由面向对象的重写理论指定，该理论包含上述类的定义和描述不同原语行为的重写规则：对象移动性，消息传递以及对象和进程创建。此规范是Mobile Maude的系统代码，它作为执行MobileMaude应用程序的原型这样的应用当然需要满足某些要求，作为面向对象的，使用__构造函数从移动对象发送消息，并使用原语消息移动到其他进程。我们现在将介绍应用程序中使用的Mobile Maude原语。对象之间有三种通信方式同一移动对象内部的对象可以通过任意格式的消息相互通信，通信可以是同步的，也可以是异步的。不同移动对象中的对象可以在这样的移动对象处于同一进程中时进行通信，也可以在它们处于不同进程中时进行通信;在这些情况下，实际的通信类型对移动对象是透明的，但是这样的通信必须是异步的，并且可以在不同的进程中进行通信。sages必须是_：_的形式，其中第一个参数是标识符第二个参数是消息内容，一个使用自由用户定义语法构建的sort Contents的值（例如，参见3.2节）。也就是说，发送消息是接收者的身份;如果发送者想要传达其标识符，则必须将其包含在消息内容中。如果收件人是不同移动对象中的对象，则消息必须由发送方对象放在其状态的第二个组件（传出消息托盘）中。系统代码将把消息发送到收件人对象。当一个移动对象想要移动到另一个进程时，它会在其传出消息托盘中放置一个go（PI）消息，其中PI是目标进程标识符。当移动对象具有传出的go消息时，在重新移动传出消息并将状态设置为空闲之后，发送新的移动对象间go消息，其中移动对象作为其自变量之一。 这确保杜兰和贝尔德霍131移动对象在移动时是不活动的。如果消息的发送者和接收者在不同的进程中，那么这个消息必须旅行到所需的进程，出去到进程的外部配置。当消息到达目的地进程时，移动对象被放入其中（处于活动模式），并且父进程被通知，因此它可以更新其转发信息，或者仅仅更新，如果它是父进程本身。在go消息中，移动对象指示它要去的进程有时，一个移动的物体想要到达另一个物体，但它只知道它想要追赶的物体的标识符，而不是它所处的过程。在这种情况下，可以使用go-find消息 当这个消息被一个对象M使用时，它把M想要到达的移动对象的标识符和它可能所在的试探性过程的标识符作为参数。当一个对象想要创建一个新的移动对象时，它会向系统发送一个newo消息（通过将其置于其状态的第二个组件中）。newo消息将一个模块M、一个配置C（这将是要被放置在要创建的移动对象的腹部的初始配置，并且是模块M中的有效项）以及配置C中的主对象的临时标识符作为参数（的元表示）。当系统检测到newo消息时，它完成的第一个动作是创建一个新的移动对象，配置C作为其状态，模块M作为其代码，然后向主对象发送一个启动消息，并使用其新名称，因此它与它所在的移动对象的名称一致描述移动对象行为的代码被称为应用程序代码，我们在这项工作中的主要目的是说明如何在开发我们的应用程序时使用这种构造，以及如何轻松地使正常的面向对象规范移动。Mobile Maude 的 系 统 代 码 以 及 一 些 相 关 信 息 可 以 在www.example.com中找到http://maude.csl.sri.com/mobile-maude。3会议评审系统我们在本节中讨论的雄心勃勃的广域应用已经被不同的作者使用[3，13]，尽管我们遵循Luca Cardelli的介绍在[2]中，他将其描述为对任何广域语言证明其可用性。问题在于管理会议的虚拟程序委员会会议图1显示了（几乎所有）会议评审过程中的不同步骤;以下描述中的数字与本图中的数字相对应。首先宣布会议（1），并公布电子提交表格。如果对提交感兴趣，作者可以获取提交表单（2），该表单在激活后（3，4，5），将指导大部分审查过程。每个作者填写表格的实例并附上一张纸（6）。一旦提交表格完成，杜兰和贝尔德霍1321. 公告20.我FSubF会议椅2.提交请求21. 终稿作者18. 恭喜36. 纸SubF5.我194RepFSubF2224. 诉讼717RevF11RevF10个SubFRepF12. 纸9. 电子邮件8. 纸13. 裁判141615. 审查审稿RevFFSubF项目主席23. 终稿Fig. 1. 会议审查进程。提交给项目主席（7），他收集提交的材料（8）并将其分配给 通过指示每个提交表单为每个指定的成员生成审查表单（9，10）。然后，每份评审表会被分配给委员会成员（11，12），委员会成员可以决定直接评审论文，拒绝评审，或将其委托给另一位评审员。评审表记录了他们经过的评审员，以便他们在完成或被拒绝时可以找到回去的路，允许每个评审员检查其子评审员的工作。最后，完成了一项审查（13）。然后，表单执行各种一致性检查，例如验证分配的分数在范围内，并且没有必填字段留空，然后它找到返回程序主席的方式（14）。一旦评审表到达程序主席，这一个累积的分数和评论每篇论文（15）。 一旦节目主持人收集了所有的评论，一份文件，这一个是解决。如果评审意见一致，项目主席宣布该表格为接受或拒绝的纸质报告表格（16）。如果报告不一致，项目主席宣布该表格为未解决的评审表格，该表格在评审员和项目主席之间循环，积累进一步的评论，直到项目主席宣布该论文被接受或拒绝。程序主席创建了一个新的报告表格，其中包含此类论文的修订结果，然后返回到 提交人（17），并表示适当的祝贺（18）或遗憾。一旦提交人收到该通知，即通知提交人审查过程的结果。一份被接受的纸质报告表格会产生一份最终的提交表格杜兰和贝尔德霍133(19，20），作者附上了论文的最终版本（21）。完成的最终提交表格会返回到程序主席（22，23），程序主席将它们合并到程序中，并让它们找到会议主席（24）。从前面的描述中，我们可以识别不同的参与者，他们可以自由地从一个过程移动到另一个过程，因此他们应该被表示为移动对象。在MobileMaude方法中，系统的规范由嵌入在移动对象中的对象组成，这些对象通过消息相互通信。 除了代表一词之外， 每个移动对象携带管理对象配置行为的代码和表示这种状态的消息。Maude中系统规范的主要区别在于，这些对象必须意识到它们位于移动对象内部，并且为了与其他移动对象（对象）进行通信或使用某些可用的系统消息，它们必须遵循适当的过程。在上面的系统描述中，也有真实的人，并且假设移动代理和这些人之间有某种交互代理人会询问人们各种信息，如姓名，论文或审查报告。在我们对系统的表示中，这些人也由具有所有所需信息的移动代理代表为了简化，我们已经最小化了消息中包含的信息，并且我们没有对它们进行加密。但是，假设所有消息都是加密的。这样的加密可以很容易地通过使用加密和解密函数来添加，如[6]所示。下面我们将为系统中出现的不同移动对象提供应用程序代码的草图虽然Mobile Maude要求每个移动对象都携带模块，并在其内部指定类和对象的行为，但出于演示目的，我们更愿意在这里按照过程发生的自然顺序给出每个模块的片段。完整的规范以及执行示例可以在[8]中找到。3.1系统的类根据上述描述，我们确定了以下参与者：作者、评审员、会议主席、项目主席、项目委员会成员以及不同类型的表格，即提交表格、评审表格、报告表格和最终提交表格。作者有属性来保存他们的个人数据，他们的论文，以及他们与之交互的提交表单的类作者|name：名称，paper：默认（纸张），subm-form：默认（中间）。属性paper和subm-form分别声明为Default（Paper）和Default（Mid），这样它们就可以有一个默认值杜兰和贝尔德霍134值为null。因此，一个作者可能有也可能没有一篇论文-事实上，一个作者可能有一组论文，但在这里我们假设一个作者最多提交一篇论文-并且一个作者只有在与一个提交表单交互时才有提交表单的标识符一个会议主席对象有一个邮件列表，即一组作者标识符，会议程序主席的标识符，以及会议记录的最终ConfChair类|邮件列表：设置（中），程序主席：中，程序集：设置（纸）。除了会议主席和程序委员会成员的标识符之外，程序主席对象还需要保存有关评审过程的信息，以及收集最终论文以组成程序的方法。审查信息包括一组已被接受但尚未收到最终论文的作者的身份证以及有关每个提交的信息。此信息由排序SubmInfo项给出，它是排序的别名Tuple（Name，Mid，Paper，Set（Tuple（Mid，Score）），Int）.的是，为每个提交它是存储的名称，标识符和论文的（联系人）作者，裁判报告的结果和回合数。每篇论文的评审信息存储在评审表中，项目主席仅保留该评审表的标识符以及该评审表为给定论文提供的分数。如果出现分歧，项目主席宣布论文未解决，并将评审表发回给评审员。在三轮没有达成协议后，项目主席将做出决定。被接受的论文的最终版本保存在程序属性中。ProgrChair类|conf-chair：Mid，pc-members：Set（Mid），审稿人：Int，subms：Set（SubmInfo），接受：Set（Mid），会议记录：Set（Paper）。审阅者可以对审阅消息给出三种不同的回答：可以委托其他审阅者，可以拒绝审阅，也可以拒绝审阅并发回结果。因此，评审员具有保留其子评审员集和之前已经看过的论文集的属性，无论它决定评审、委派或拒绝它们。类检查器|次审阅者：Set（中），done（完成）：Set（纸）。程序委员会成员是评审员的特殊情况，他们不需要任何额外的属性。我们可以通过声明类PCMember为Reviewer的子类来建模这种关系，如下所示。类PCMember。子类PCMember（to O：start）Conf&none=>Conf&broadcast（OS，announcement from：O）.注意__构造函数的使用 由于通知消息被发送到ConfChair对象所在的移动对象之外的对象，因此它们被放置在其右侧。规则review-process-starts仅在此传出消息托盘为空时应用，以确保已处理任何先前的消息。 _&_操作符是表示移动对象状态的项的顶部操作符，因此，由于在其左侧可能有其他对象和消息，我们包含一个排序为Configuration的变量Conf来匹配其余部分。还要注意一个对象如何以完全透明的方式与其他移动对象中的对象进行通信，这些对象可能处于不同的进程中本示例其余部分中的大多数通信将在进程内部进行，将所述移动对象移动到它们想要通信的对象所在的进程。当一个author对象接收到通知时，它决定是否请求提交表单。这样的决定通过可以应用的一对规则之间的非确定性选择来建模。他们通过向会议主席发送subm-request消息来请求表单，然后会议主席创建相应的表单并将其发送给作者。rl [author-gets-announcement]：< O：作者|paper：P >（to O：announcement from：&O '）无=>< O：作者|> Conf&（to O '：subm-request from：O）.rl[author-gets-announcement]：< O：作者|>（to O：announcement from： O：Author|>。注意，由于最后一条规则并不意味着从移动对象发送任何消息，因此我们不需要使用__操作符来包装整个状态。当conference chair对象收到一个subm-request消息时，它创建一个提交表单，然后必须找到对应作者的方法。newo消息允许移动对象的腹部中的 对 象 创 建 另 一 个 具 有 给 定 初 始 配 置 和 模 块 的 移 动 对 象 。 模 块SUBMISSION-FORM包括3.1节中给出的SubmForm类的声明和描述其行为的规则rl [conf-chair-receives-submission-request]：< O：ConfChair|程序主席：O '>（toO：subm-request from：=>Conf&newo（up（SUBMISSION-FORM），< tmp-id：SubmForm |author：O “ ，c o n f - c h a i r ： O ， p r o g r -c h a i r ： O ” ， a u t h o r -n a m e ： n u l l ，杜兰和贝尔德霍137paper：null， state：inactive >，tmp-id）。如第2节所述，MobileMaude遵循将移动对象中的“主”对象命名为移动对象的惯例必须将信息转移到它的肚子里下面的规则启动允许SubmForm对象在收到启动消息时更改其临时名称。更改对象的名称意味着在规则的左侧销毁对象，并在其右侧创建一个具有不同名称的新对象，因此必须显式地给出所有属性rl [启动]：< tmp-id：SubmForm|作者：o（PI，I），状态：不活动，conf-chair：（to tmp-id：start-up（O））配置无=>< O：SubmForm |author：o（PI，I），state：towards-author，conf-chair：Conf & go-find（o（PI，I），PI）.当提交表单被创建时，它被置于towards-author状态，并发送消息go-find（o（PI，I），PI），以向其移动对象传达它必须找到指向标识符为o（PI，I）的对象的方式，该对象是它被分配给的作者表单创建后，它可以启动验证过程。但是，提交表单必须在本地与作者进行通信，也就是说，表单到达作者的进程后，必须开始它们之间的消息由于Mobile Maude保证从一个进程移动到另一个进程的移动对象是空闲的，我们知道，一旦在启动规则中给出了go-find命令，表单对象将无法做任何事情，直到它嵌入的移动对象被设置为活动，也就是说，直到它到达作者因此，由于没有规则如果SubmForm对象处于towards-author状态，并且传出消息托盘为非空，则该对象在到达目的地之前不会执行任何操作一旦表单到达其对应的作者，验证过程就通过发送subm-form-gets-to-author消息开始。然后，表单进入非活动状态，并且一直处于这种状态，直到它从作者那里得到一个activate-subm-form消息。rl [request-activation]：< O：SubmForm|author：O '，state：towards-author >& Confnone=>Conf&（toO '：subm-form-gets-to-author from：O）.当作者收到这样的消息时，它会发回一条消息以激活表单，并以这种方式启动提交过程。然后，提交表格要求提交作者当提交表单接收到包含名称和论文的消息时，它的相应属性将被更新，然后它将移动到杜兰和贝尔德霍138主持人请注意，N和P分别是Name和Paper变量，因此，如果存在与此规则匹配的规则，则是因为name和paper不再为nullrl[move]：无&会议=> Conf&go-find（o（PI，I），PI）.提交表单对象通过从：O'向O：submNO“”P发送消息来通知程序主席它的到达在收到这样的消息后，ProgrChair对象向其注册提交集添加一个条目，并将其分配给其属性审阅者给出的委员会成员数量。程序主席要求提交表单为每个分配的委员会成员创建一个审查表单，方法是向提交表单发送一个gen-review-forms，其中包含程序委员会的选定成员。3.3审查过程审查表格是用newo消息创建review-forms操作负责生成这些newo消息，每个消息对应一个要生成的请注意，评审表创建后将尝试联系的计划委员会成员的标识符将作为评审员链中的第一个optical-review-forms：Paper Mid Set（Mid）-> MsgSet.eq-审查-表单（P，O ' ， m t ） = 无 。eq-审查-表格（P，O '，O“。OS）= newo（up（REVIEW-FORM），< tmp-id：ReviewForm|状态：非活动，分数：空，程序主席：O '，链：O“，chain-back：no-id，rejected：mt，paper：P>，tmp-id）审查表（P，O ' ， O S ）。rl [gen-review-forms]：（to O：gen-review-forms （OS ））Confnone=>< O：SubmForm|状态：完成>会议&审查表格（P，O '，OS）。当一个评审表单到达它正在寻找的评审者的流程时，首先是一个程序委员会成员，它向给定的评审者发送一个评审消息并等待答案。审阅消息包括它不能委托的审阅者集合作为参数，包括它以前传递过的所有审阅者，为了避免循环，不应该再次使用，以及那些已经拒绝审阅的审阅者。 函数listToSet返回一个集合，其中包含 列表作为参数。rl [要求审查]：Confnone=>< O：ReviewForm|状态：未激活>会议&（toO '：review P excluding（listToSet（OL）. OS）from：O）.如果审阅者拒绝审阅，则审阅表单必须返回到最后一个委派的审阅者，并将拒绝者添加到rejected属性中的集合rl [review-rejected]：（toO：cannot-review）确认无=>< O：ReviewForm|状态：towards-reviewer，链：OL&o（PI，I），拒绝：OS。O&' > C o n f g o - f i n d （ o（ P I ， I ） ， P I ） .一旦获得评审，取决于链中是否只有一个或多个评审员，该表格将返回到程序主席（如果只有一个，则是程序委员会成员本身）或返回到委派的评审员。rl [review-result]：< O：ReviewForm|状态：背部，得分：Sc，chain：OL&&&O '，chain-back：o（PI，I）OL' > Conf go-find（o（PI，I），PI）.在返回的过程中，每个审阅者都会检查该审阅。评审表通过每个评审员的流程，每次到达新评审员的流程时，它都会请求评审员进行检查，这可能会确认或反驳评审。当评审表单返回到程序主席的流程时rl [pc-gets-review-result]： （ t oO ：r e v i e w - r e s u l tPS cf r o m ：O ” ）=>。当程序主席有所有的裁判报告提交，它必须得到解决。如果评审意见一致，则论文被接受或拒绝。否则，也就是说，如果评审意见不一致，则项目主席宣布评审表未解决，并将其发回给项目委员会的成员。经过三轮评审后，项目主席决定提交决定大多数评审员的决定。crl [disagreement]：< O：ProgrChair|subms：（（N，&O '，P，TS ，I）Subms ），reviewers ：I' > Confnone=> 会 议 广 播 （ 审 阅 者 （ T S ） ， 未 解析 ）如果大小（TS）== I <' 且 I 2 且 不 一 致 （ T S ）。杜兰和贝尔德霍140如果评审意见一致或轮数达到限制，项目主席将创建一个报告表，该报告表将返回给作者，并向与本文相关的所有评审表发送终止消息如果存在一致意见，则决策函数返回一致同意的分数，否则由多数人决定。如果不同意一个均匀的结果，那么论文被接受。CRL[协议]：< O：ProgrChair|subms：（（N，&O'，P，TS，I）Subms），accepted：OS，reviewers：I'>Confnone=> Conf&newo（up（REPORT-FORM），，tmp-id）如果大小（TS）== I'且（一致性（TS）或I== 2）。3.4报告过程当一份被接受的论文报告表格到达作者时，它会发送一条祝贺消息，并将自己转换为最终提交表格，该表格将要求作者提供论文的最终版本。注意我们是如何将ReportForm类的对象转换为FinalSubmForm类的对象的。这种内部对象保持其标识符的事实使得在某个点上是报告形式的移动对象成为最终提交形式的移动对象。rl [send-congratulations-and-transform-into-a-final-form]：Confnone=> Conf（to O'：congratulations）.最后，最终提交表格与论文的最终版本将其发送到程序主席，这将合并到诉讼文件。当所有被接受的论文的最终版本都到达程序主席，并且没有未解决的提交时，程序主席将会议记录发送给会议主席。4相关工作虽然Cardelli提出这个案例研究是对移动语言的挑战，但它是一个众所周知的例子，经常用于工作流程管理领域[10]协调语言。本文[10]描述了这个案例研究（例如我们已经实现了它是一个行政工作流程，即它涉及重复的、可预测的过程，具有简单的任务协调规则，其中任务的排序和协调可以自动化。杜兰和贝尔德霍141在[15]中，提出了一种使用M anifold的案例研究模拟解决方案，MANIFOLD是一种强类型，块结构，事件驱动的协调语言，其中通信是异步的，并且计算和通信关注点的分离得到了强有力的执行。这种方法将应用程序结构化为一个以协调器和协调的过程区分的过程层次结构，并专注于可以自动化和协调的过程作为一个需求规范，本文不涉及移动性，作者认为这是一个实现问题。论文[14]提出了一个更接近我们的解决方案，使用活动（移动）文档的概念它使用PageSpace架构，这是一种基于Web的应用程序的设计范例，该应用程序由自治代理组成，无论其物理位置如何，都可以执行其职责。这个架构是实例化与移动设施的协调语言。它遵循MUD（多用户地下城）的隐喻，一个合作的互动环境，由几个人共享社交和互动。它基于房间、物品和玩家（或用户）的概念，这些概念与我们的过程和移动对象的概念有关。还描述了实现该应用的实际系统。该文件[13]描述了为第四届和第五届国际万维网会议开发的电子管理系统。5结论我们已经展示了如何移动Maude，Maude支持移动计算的扩展，可以用来表示和指定雄心勃勃的广域应用程序，通过提供一个会议审查系统的实现Mobile Maude的语义通过一小部分重写规则以独立于应用程序的方式定义。除了允许我们执行移动系统，证明它们的属性等，这种可执行的Maude规范可以让我们识别可能的缺陷，并尝试不同的替代方案。例如，去寻找消息没有在系统消息的原始集合。 此外，我们认为，应该在Mobile Maude中引入，特别是允许新类型的代理通信和交互。例如，如果一个对象在与另一个对象交互时移动到另一个进程，会发生什么？也许，移动对象内部的对象和它所在的进程之间应该有某种通信，比如询问另一个移动对象是否也在同一进程中，或者询问进程在另一个对象离开或到达时的通知。此外，我们可以考虑支持面向组的事件（其中消息被发送到一组移动代理中的所有成员）和协作（其中协作者代理和代理组被定义并相互交互以获得共享目标），如Concordia系统[16]。作为未来的工作，我们要考虑验证移动的属性，杜兰和贝尔德霍142系统，特别是与其可靠性和安全性有关的系统。在这个方向上有趣的贡献是模态逻辑重写逻辑的作品[9]和空间逻辑的工作[1]。确认作 者 感 谢 StevenEker ， PatrickLincoln 和 Jos′eMeseguer ， 我 们 正 在 开 发 MobileMaude，对会议审查系统的规范进行了许多讨论。我们也非常感谢Narciso Mart-Oliet和Roberto Bruni对该文件的几个草案和应用程序的具体说明提出了建设性的意见我们还要感谢匿名推荐人带领我们开展相关工作。引用[1] L. Caires和L.卡德利并发的空间逻辑（第一部分）。计算机软件的理论方面，TACS 2001，LNCS 2215，第1-37页。Springer-Verlag，2001.[2] L. 卡 德 利 移 动 计 算 的 抽 象 在 j.Vitek 和 C.Jensen ， Secure InternetProgramming：Security Issues for Mobile and Distributed Objects，LNCS 1603，51-94页。Springer-Verlag，1999.[3] P
