电子笔记在理论计算机科学50第3期（2001年）。GT-VMT 2001网址：http://www.elsevier.nl/locate/entcs/volume50.html9页规范的图变换观使用Mobile Code的应用程序？Andrea Corradini1Dipartimento di Informatica，Universita di Pisa，Pisa，ItalyFernandoLu sDottiFaculdade de Informatica，Pontif cia Universidade Catolica do Rio Grande do Sul，巴西莱拉·里贝罗3巴西南里奥格兰德联邦大学信息学院摘要这个扩展摘要的主要目的是讨论规范的要求-分析了图转换系统在多大程度上可以满足这些需求。我们提出了一些扩展的理论图变换似乎是可取的，以应付这种应用程序。1引言高度分布式的网络（如Internet）已经成为大规模分布式编程的通用平台.这些环境通常被称为开放环境，其特征是：大规模地理分布;高动态性（新节点和服务的出现）;没有全局性？ 研 究 部 分 由 ForMOS项 目 （ M etodos Formais para Codigo Movel em SistemasAbertos）-grant CNPq 520269/98-5，研究培训网络GET-GRATS（图形转换系统的一般理论）和MURST项目Teoria della Concorrenza，Linguaggi di Ordine Questionore eStrutture di Tipi（TOSCA）支持。1 电子邮件地址：andrea@di.unipi.it2 电子邮件地址：fldotti@inf.pucrs.br3 电子邮件地址：leila@inf.ufrgs.brc 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗控制;部分故障;由于通信链路的多样性（延迟、吞吐量）、合作组织、所提供的服务等，缺乏安全性和高度异质性。研究工作已被定向到通过开发新的范例，理论和分布式应用技术来管理这种复杂性。在这种情况下，代码移动性[11]由于其灵活性和在各种应用领域中的潜在用途而受到特别关注，如网络管理[11]，电子商务[19]，分布式信息检索[16]，高级电信服务和主动网络[27]，主动文档，工作流管理系统和断开操作（即，启动远程计算，切换到本地节点（例如，膝上型计算机），稍后接通节点，并接收远程计算的结果）。目前有标准，平台和语言可用于移动代码[22]。Java由于其高可移植性和动态绑定等特性而得到广泛使用然而，为了建立对移动代码的良好支持，仍然存在需要解决的问题。 其中之一就是缺乏正式基础：围绕移动代码和主动网络及其实现的想法来自于一种实用的方法。一个抽象的语义框架（包括规范，验证和分析的方法），以形式化的计算模型的互联网应用程序显然是需要的，和缺失。这样的语义框架可以提供形式化的基础来讨论和激发有争议的设计/实现问题，并以严格的方式陈述和证明属性。图转换系统被用作规范形式主义，以及描述并发和分布式系统的计算模型[24，9，10]。在这个扩展的摘要中，我们将讨论图变换领域的现有概念在多大程度上可以用于描述开放环境中的移动代码系统，并给出适当扩展的想法2移动代码应用程序和开放环境在移动代码应用程序的典型环境中，分布式环境包括一组位置和一组移动组件：位置代表支持移动应用程序所需的基础设施。该基础设施包括硬件和软件（中间件）支持，以提供移动组件可以运行、移入和离开的位置。除了这些基本功能之外，还可以根据需要配置位置以支持其他功能。在构建移动应用程序时，开发人员假定放置了给定级别的功能。最低级别是对同一地点各组成部分之间的流动性和通信的支持。3GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗移动组件是软件组件，在其执行期间，可以从一个地方迁移到另一个地方以使用其他组件以及基本设施，如处理能力，存储和通信。移动组件具有内部数据或状态、代码以及一组元数据或属性（例如，标识符、凭证、发起者、操作状态等）。移动应用程序可以由各种移动组件构建，这些组件可以同时运行并协作。在为开放环境开发移动代码应用程序时，必须考虑以下主要特征开放/动态环境：位置必须具有基本的功能级别，并且易于配置，以便更好地实现分布式基础设施的目标。 在许多情况下，位置必须是高度可定制的，以便在分布式环境中支持不同的应用程序。重要的是要在不同的地方轻松安装组件，并在之后使用它们（例如，用于主动网络）。所考虑的分布式环境的特点是开放的。软件组件和位置是独立的，因为它们具有不同的所有权，因此具有不同的权限来决定它们的管理。在这样的环境中，这些实体具有不同的生命周期，并且不能提供/获得全局状态。尽管如此，各实体往往为了实现其目标而相互合作。无位置透明性：零部件设计时没有位置透明性。迁移不是透明的，而是明确指定的自治/并发：组件可以创建其他移动组件，并在相同或不同的地方并发运行。由于每个组件的自治性，重要的是独立地设计/表示每个组件。模块化/协作：重要的是要有良好的组件接口，并能够组合各种组件来构建应用程序。失败：在设计分布式应用程序时，设计者必须考虑应用程序运行环境的某些行为这一点已经在地方上说明了另一个非常重要的方面是考虑环境的失效行为因此，希望设计者可以陈述环境的预期故障行为，并构建其应用程序来处理它。3图形转换视图图转换系统允许将分布式系统的状态表示为图，并通过重写规则的本地应用对此类系统的计算进行建模。拓扑的显式表示4GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗使得该形式体系特别适合于指定移动代码应用，因为基本信息不需要被编码，而是可以以直接和直观的方式被处理。在本节中，我们将依次考虑前一节中列出的移动代码应用程序的每个特征，并针对每个特征讨论图转换系统在多大程度上足以对其进行建模，以及可能需要哪些扩展。没有位置透明性：位置的指定可能是隐式的或显式的。例如，位置的隐式表示用于微积分[20，21]和移动环境[2]。 这使得模型更加独立于实现，但也使得实现规范更加困难。位置和组件标识的显式表示似乎更接近当前的实现平台。使用图形转换系统，很自然地将地点和组件建模为节点，并将空间分布建模的关系（如地点的相邻性，地点上组件的存在，...）作为边缘。实际上，有一个系统的拓扑结构的显式表示的可能性是一个优点，有利于这种规范形式主义。自治/并发：典型地， 一个移动代码应用程序是特殊的，在不同的组件方面，这些组件自主地、并发地工作组件之间通常通过消息传递进行交互，并在执行过程中创建新的组件。图变换系统允许人们通过规则来描述分布系统的演化，这些规则在应用时具有局部效应。并发在很大程度上是内置的，因为独立的局部修改可以以任何顺序执行而不会影响结果[1]。目前还没有消息传递的自动建模，但是在文献中有各种关于使用图变换对基于消息传递的系统进行建模的合理建议[15，17，23，4，5]模块化/合作：移动代码应用程序的完整规范需要指定各种组件以及指定中间件（位置）。在现实情况下，单块规范很难管理和维护。通常，中间件可以单独指定，并且该规范可以在许多系统中重用。此外，系统的各种组件可以由不同的人/组独立指定。因此，模块化概念必须得到规范形式主义的支持。一个模块必须有一个导出接口，该接口至少提供它所实现的组件的行为的抽象描述。在实际应用中，这通常是由传递给其他组件的函数（方法）的签名给出的[18]。图形转换系统的模块化设计有多种方法5GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗[8]见《易经》，见《易经》。在所有这样的方法中，模块至少包括由模块处理的图的类的描述（例如，经由类型图）和图变换规则的集合。关于导出接口，一些方法（如GRACE [14]和PROGRES [25]）只允许导出程序名称，而其他方法（如DIEGO [26]和TGTS [12]）也允许导出规则。 此功能可用于根据可观察事件的种类（例如，组件接收/发送的消息）抽象地描述组件的行为。这将允许一种可靠的担保方法[6]。与复杂系统规范的所有方法一样，规范形式主义需要具有形式化语义，该语义可用于验证规范并验证其是否符合移动代码应用程序的要求。这样的语义应该是组合的：通常整个系统的语义应该作为构成系统本身的模块的语义的适当组合来获得。在理想情况下，模块的导出接口还将包括关于导出的规则/过程的语义信息，并且形式主义将支持模块的正确性的概念，确保接口中描述的抽象语义与规范的规则所描述的语义一致。开放/动态环境：将应用程序分解为不同的模块还不足以指定移动应用程序，因为组件将执行的环境是高度动态的（位置和其他组件可以随时创建/删除），这意味着移动应用程序的规范不能遵循“封闭世界规则”。因此，这种应用程序需要一个开放的，松散的语义。[13]中提出的语义框架似乎满足了这些要求中的大部分。动态环境：在许多情况下，允许创建同一组件的多个实例是很有趣的。例如，如果有一个要访问的地方的列表，要求一些信息，那么可以创建一个移动组件来访问每个地方并带回信息。他们之间唯一的区别是他们要去的地方。图转换中的模块化的一些方法允许为模块指定形式参数例如，在PROGRES和CGSPEC [7]中，由模块导出的过程可能具有可以在实例化时由客户端绑定的参数。组件可能在任何时候死亡，即使其他组件有指向它们的指针（例如，知道它们的名称）。中间件负责处理这些情况：如果组件试图与不存在的组件通信，它会发出警告。此外，中间件可以支持分布式垃圾收集。在这种情况下，组件不会死亡，但可能6GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗停止其内部活动，并仍然对来自其他组件的消息作出响应。 当其他组件不再引用该组件时， 然后它可以被分布式垃圾收集擦除在图转换方法中，处理组件删除的一种可能方法是将它们标记为死的，并提供（异常）规则来处理组件试图与它们通信的情况。 这些规则以及分布式垃圾收集规则（如果有的话）应该是中间件规范的一部分，因为这是由该级别提供的服务。希望语义以一种干净的方式处理异常。失败：移动代码应用程序必须应对开放环境的不可靠性。通常情况下，人们应该在实施这些系统时提供一定程度的信任。例如，人们可能希望确保在没有任何故障的情况下，系统按预期运行;或者如果某些服务器（必须指定）发生故障，系统仍然正确运行，等等。本文提出了一种图形转换系统的静态分析方法。在[3]中提出，其中使用修改的展开构造，从给定的系统的一个尼特图可以与一个底层的Petri网一起提取。从系统的初始图可到达的所有图都可以同态映射到提取的图，因此可以用于检查所有可到达图的由态射反映的适当性质（如不存在路径或循环）。此外，底层网概括了系统规则之间的一些因果依赖关系，并且可以使用标准Petri网技术进行分析，从而提供关于原始系统的附加信息。该技术在移动代码应用中的应用是未来研究的主题4总结发言在前面的部分中，我们非正式地讨论了移动代码应用程序的一些特征方面，这些方面应该通过特定的阳离子形式主义旨在描述这样的系统。我们认为图转换系统是实现这一目标的一个很好的候选者，并解释了它们以直接的方式支持一些所需功能的方式。对于其他方面，即使文献中的各种建议从不同的角度解决这些问题，肯定还需要做更多的工作。本着研讨会的精神，这一扩展摘要是书面的，目前的贡献主要是方法论。我们打算追求的研究方向包括选择一种特定的方法来进行图转换，尽可能多地满足上一节中挑选出的属性，并使用它来实验示例移动代码应用程序的规范。7GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗在[4，5]中报告了在这个方向上的第一次尝试，其中使用了一种受限形式的图语法来建模代码移动性。组件、位置和消息被建模为节点。位置的行为由实现典型中间件功能的规则指定，例如将消息转发到位于远程位置的代理，或处理代理的迁移。每个组件的行为都是以反应的方式指定的：每个规则必须删除一个消息顶点，这意味着该消息触发该规则的应用。规范中没有使用真正的模块概念，但对规则有一些进一步的限制，以确保组件的封装属性。引用[1] Baldan，P.，Corradini，A.，Ehrig，H.，L哦，M.， 莫恩塔纳里，美国。Rossi，F.代数图变换的并发语义[10]。[2] 卡尔代利湖和Gordon，A.，移动环境，软件科学和计算结构的基础，计算机科学讲义，卷。1378，Springer，1998，pp. 140{155.[3] Baldan，P.，Corradini，A.和Konig，B.，A Static Analysis Technique forGraph Transformation Systems，2001.[4] Dotti，F.和里贝罗，L.，基于 图形 语法的 移动 代码系 统的 规范，Proc.FMOODS'00 Formal Methods for Open Object-based Systems，斯坦福大学（美国），Ed. Kluwer，2000年（即将出版）。[5] Dotti，F.和里贝罗，L.，开放系统中的代码移动性：一种正式的方法。PDPTA'00并行和分布式处理技术及应用，拉斯维加斯（美国），2000年。[6] Duarte，C.H.C.和Maibaum，T.，开放分布式系统设计的可靠保证规程，信息处理快报，第74卷，2000年，pp. 55{63.[7] Ehrig，H.和Engels，G.，图转换系统的模块概念的语用和语义方面，在第五届国际会议论文集。图文法及其在计算机科学中的应用研讨会137{154.[8] 赫克尔河，Engels，G.，Ehrig，H.和Taentzer，G.，图变换系统模块度概念的分类与比较。在[9]中，pp. 669{690.[9] Ehrig，H.，Engels，G.，Kreowski，H. J.和Rozenberg，G.（编辑），手册的图语 法和计 算通 过图 形 转 换 ， 第 2 卷：应用程序、语言和工具。World Scienti c，1999.8GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗[10] Ehrig，H.，Kreowski，H. J.，蒙塔纳里湾Rozenberg，G.（编辑），图形 语法 和计 算的 图形 转 换手 册， 第3 卷 ： 并发 性， 并 行 性和 分布。WorldScienti c，1999.[11] Fuggeta，A.，皮科湾和Vigna，G.，理解代码移动性，Trans.《软件工程》，IEEE，第24卷，1998年，pp. 342{361.[12] Gro e-Rhode，M.，Parisi Presicce，F.和Simeoni，M.，类型化图转换系统 的 元 素 和 ， 在 Proceedings WADT'98 ， Lecture Notes in ComputerScience，vol.1589，Springer，1999，pp. 137{151.[13] 赫 克尔 河， Open Graph Transformation Systems ：A New Approach to theCompositional Modeling of Concurrent and Reactive System（开放图转换系统：并发和反应系统组合建模的新方法）论文，柏林工业大学，1998年。[14] 赫克尔河，何曼，B.，Knirsch，P.和Kuske，S.，GRACE的简单模块，在Proceedings TAGT'98，Lecture Notes in Computer Science，vol. 1764，Springer，2000，pp. 383{395.[15] Janssens ， D. Rozenberg ， G. ， Actor Grammars ， Mathematical SystemsTheory，vol. 22，1989，75{107.[16] Knudsen，P.，两种分布式计算范例的比较-性能案例研究。1995年，特罗姆瑟大学，硕士论文[17] Kor，M.，广义图结构及其在并发面向对象系统中的应用.论文，柏林技术大学，1995年。[18] Lange，D.B.和张。D.T. Java Aglet应用程序编程接口（J-AAPI）白皮书。IBMCorporation.1997年11月，http://www.trl。ibm.co.jp/aglets/JAAPI-whitepaper.html。[19] Merz，M.和Lamersdorf，W.，代理、服务和电子市场：它们如何结合？分布式平台国际会议论文集，IFIP/IEEE，1996年。[20] 米尔纳河Parrow，J，A calculus for mobile processes I，Information andComputation，vol. 100，1992，pp. 1{40.[21] 米尔纳河，Parrow，J.和Walker，D.，A calculus for mobile processes II，Information and Computation，vol. 100，1992，pp. 41{77.[22] Perdikeas，M.，Chatzipapadopoulos，F.，韦涅里斯岛和Marino，G.，移动代 理 标 准 和 可 用 平 台 。 ， Computer Networks ， 第 31 卷 ， 1999 年 ， pp.1999{2016.[23] L. 里贝罗，图文法的并行合成与展开语义。论文，柏林工业大学，德9国，1996年。[24] 罗森伯格湾（编辑），图形语法手册，卷。1：《世界科学基金会》，1997年。10GT-VMT 2001 {A.Corradini，F.Dotti，and L.里贝罗[25] 史 昌 湖rr ， A.和 Wi nter ， A.J. ，UMLPackagesforPROg rammedGraphREwritingSystems ， in Proceedings TAGT'98 ， Lecture Notes inComputer Science，vol. 1764，Springer，2000，pp. 396{409.[26] T ae ntzer，G. 关于SCHUrr，A.，张文，“图变换系统的一种新的数学模型”，载《图的重写与计算学报》，第2期，1995年，http：//www.elsevier.nl/locate/entcs。[27] Tennenthouse，D.L.，Wetherall，D.J.，史密斯，J。M.，明登湾J. 和Shiaskie，W.，主动网络研究综述，IEEE通信杂志，1997年1月。
我的内容管理
展开
