“基于图变换的形式化服务规范与匹配方法”

理论计算机科学电子笔记105（2004）37-49www.elsevier.com/locate/entcs一种基于图变换的形式化服务指定与匹配方法R. Heckel，A. Cherchago，M. Lohmann1帕德博恩大学计算机科学、电气工程和数学系德国帕德博恩摘要当Web服务由链接服务提供者和请求者组成时，请求者对“有用”服务的需求必须与供应商。除其他事项外，服务规范（要求或描述）可能包含操作合同，规定（要求或提供的）操作的先决条件和效果在本文中，我们提供了一个半正式的，基于UML的符号合同和合同匹配，以及这些概念在图变换方面的形式化。 我们建立了请求者和提供者规范之间所需的语义关系，并证明了我们的句法匹配w.r.t.概念这种关系。保留字：Web服务，合约匹配，图转换1介绍互联网，或者更具体地说，WWW，为熟练的人类用户提供了几乎无限的信息和服务来源。我们可以翻译文本，获取度假胜地的温度信息，预订机票，订购旅游指南，而无需离开电脑。更令人惊讶的是，我们甚至不需要知道谁会为我们提供这些服务。知道谷歌通常会迅速找到我们需要的服务器。Web服务的最终愿景是将这种能力转移到程序中。这些程序应该能够在运行时通过网络定位和调用服务1电邮地址：【 玲子|切尔恰戈|mlohmann]@upb.de1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.05.00638R. Heckel等人理论计算机科学电子笔记105（2004）37来实现他们自己的目标这包括两个问题：如何找到这些服务以及如何使用它们。 在本文中，我们将重点讨论如何找到它们的问题。当前的Web技术已经支持大部分的发现过程：被操作的服务的接口（通常是要调用的方法）可以用Web服务描述语言（WSDL）来指定。这个规范和一些描述Web服务基本信息的关键字可以在中央UDDI服务器上注册。该登记处充当中央信息中介人，应客户的要求然而，一个非常重要的问题仍然是开放的：客户或客户应用程序如何找到与客户需求相现在这个问题的答案相当简单：开发人员在UDDI服务器上查询一个服务，从结果中选择一个合适的服务，并将这个服务的调用集成到他的程序中（例如WebSphere Studio [6]支持）。 在运行时，程序只能尝试执行选定的服务。如果此服务不可用，例如由于网络问题，程序甚至不能自动发现相同的替换服务。这与动态发现适当服务的想法相去甚远。因此，建立最大程度地自动化发现过程的技术是非常重要的。在我们的工作中，所提供和所需服务的兼容性是通过构成服务接口的操作之间的兼容性来定义的。对于所有必需的操作，有必要找到结构和行为上兼容的提供操作。 结构兼容性要求提供的操作签名和要求的操作签名之间的对应性。这可以使用从软件组件库中检索函数和组件的技术来检查[12]。我们专注于第二个问题-行为兼容性。服务请求者和提供者通过契约指定关于其操作的行为信息[5]。我们建议使用图转换规则进行合同指定。基于图变换的双推出（DPO）方法[4]的规则的经典解释不足以满足此目的。它假设在转换中没有任何变化超出规则中明确指定的范围。然而，运营合同代表了一个潜在的不完整的转换规范已经提出了图转换，以提供对图转换规则的更宽松的解释。双回调（DPB）方法[7]定义了图形转换R. Heckel等人理论计算机科学电子笔记105（2004）3739并通过允许额外的改变来推广DPO，而不是在规则中编码。这种规则解释适用于指定操作合同的规则。基于图转换的概念，我们将定义对提供者规则匹配请求者需求意味着什么的操作理解。这将在语义匹配关系中捕获。由于这种关系是建立在无限个转换集的基础上的，不能直接计算，我们引入了一个句法匹配关系，它为语义匹配关系提供了一个充分条件。在下一节介绍了服务规范和示例应用程序的基本思想之后，在第3节中，我们将讨论服务规范匹配的问题，重点是所提供的和所需的操作契约之间的兼容性。部分形式化的这些概念，包括健全的句法关系w.r.t.语义的一个，将在第4节中给出。在第5节中，我们总结并列出了形式化中的开放问题。2服务规范在本节中，我们考虑服务规范的基本成分，并介绍一个汽车租赁系统的Web服务场景我们从图1中的UML类图表示的应用程序的数据模型开始：一个租赁公司（ 类RentalCompany ） 拥有不同类型（ 类Truck 、 Car 、 Van 、Jeep）的车辆（类Vehicle）。如果客户（客户类）想要租用车辆（协会租赁），则需要预订车辆（协会预订）。每个法律实体，即客户或公司，都有名称、地址和银行账户。客户和公司之间的关系由一个包含所有相关租赁信息的合同（类EContract）来管理，例如租赁期（类RentalInfo）。为了避免额外的复杂性，我们假设服务请求者和提供者使用相同的数据模型，并事先达成一致。”A Web service is an interface that describes a collection of operations thatare network-accessible through standardized XML messaging” [服务规范的下一提供的和所需的接口的示例如图所示二、接口包含有关操作的结构信息，而这些操作的属性可以由合约指定合同的概念[5]在Web服务社区中被广泛用于描述服务及其组成部分的行为合同由一个前提条件组成，40R. Heckel等人理论计算机科学电子笔记105（2004）371. *具有10..11制造商*0.. 1电子合约已签署：Bool* 执行10..十...10..1110.. 1constructedBy1.. *储备金**拥有Rid：String车辆pick-upDate：DatereturnDate：Date租赁信息RenatlCompany1提供客户name：String地址：字符account：blz：中国合法实体银行信息⇒makeReservv（c：Customer，car：Car，ri：RentalInfo）：EContract makeCntr（ec：EContract，bi：BankInfo）：EContract changeCntr（ec：EContract，car：Car，ri：RentalInfo）：EContractb. 。r e. akCntr（ec：EContract）<<联系方式>>ProvidedInterfacereservCar（cus：Customer，my_car：Car，ri：RentalInfo）。r e. n. tCar（ec：EContract，bi：BankInfo）<<联系方式>>企业简介ents*卡车车Van吉普Fig. 1. 汽车租赁公司系统的数据模型。图二. 提供和要求的接口。在执行某个行为之前确定系统状态，以及在执行该行为之后描述系统状态的后置条件。有不同的方法采用正式的技术（例如，描述逻辑[11]、情境演算[10]、代数规范语言[12]等）合同具体化。 这些方法的主要障碍是它们缺乏可用性在软件行业中，逻辑形式主义的应用知识和技能是稀缺的。相反，我们寻求一种接近标准软件建模语言的符号（例如，UML），同时具有允许提供自动化的正式背景。这种契约的可视化形式化符号是由类型化图转换[2]提供的。在这种情况下，类图被认为是一个有向属性图，其顶点包含类型和属性声明。它们与表示运行时状态的对象图的关系由类型图（T G）和相应的实例图的概念表示[2]。 图变换规则p：LR由一对具有相容结构的TG型实例图L，R组成，使得出现在L和R中的边连接到两个图中的相同顶点，具有相同名称的顶点具有相同类型，等等。图的一部分3由虚线矩形标记有时，需要单独指定R. Heckel等人理论计算机科学电子笔记105（2004）3741让提供小液提供p=>建设者储备L^pLpRpreservCar（cus：Customer，my_car：Car，ri：RentalInfo）=>储备L^rLrRrmy_car：cabcus：Customercus：客户汽车：Carri：RentalInfoec：EContractc：Customerri：RentalInfoc：客户my_car：cab汽车：Carmy_car：cab汽车：Carcus：Customerri：^lrmakeReservv（c：Customer，car：Car，ri：RentalInfo）：EContractc：Customerprovidesri：RentalInfo图三.提供的操作makeReserve和必需操作的图形转换规则预订汽车。规则的应用。 在这种情况下，图变换规则具有正应用条件P：使用LLR。 除了T G-typed实例图L和R，p表示图L，该图L通过应用所需的元素指定L的扩展，但不以其他方式使用。（参见图3）。图3展示了所提供的操作makeReservv和所需的操作reservC ar的图形转换规则。 Lp和Lr包含表示操作的输入参数的三个节点：关于客户的信息（顶点c和cus）、租赁期（顶点ri）和运输单元（顶点car和我的车）。预留由连接客户与汽车的边预留表示该边出现在Rp和Rr中，并且表示操作执行的结果。所提供的操作还创建顶点ec：EContract，显示限制汽车可用性的合约（边constructedBy）。操作makeReservv的上规则和签名表示保留操作的一个可能变体。另外三个变体可以通过同时用超级类型Vehicle（即Jeep、Van、Truck）的顶点和参数替换规则中的Car类型的顶点和签名中的Car类型的参数我们不能使用Vehicle（车辆）类型，因为汽车租赁合同必须包含运输单位的精确规格。总而言之，服务规范由数据模型、构成服务的操作的结构（操作签名）和行为（由图转换规则表示的操作契约）规范组成。在下一节中，我们将讨论服务规范匹配，并考虑一个匹配所需和所提供的操作契约的示例。42R. Heckel等人理论计算机科学电子笔记105（2004）373质量标准匹配一般来说，规格匹配必须处理规格的所有三个方面，即，数据、签名和合同。为了简单起见，我们忽略数据模型的匹配，只简单地讨论签名的匹配（参见[12]的一般讨论）。作为示例，我们考虑所需操作reservCar和所提供操作makeReservv之间的关系，makeReservv的签名和契约在图2和图3中相应地描绘。仅在提供的操作中存在的结果类型的操作签名。这并不违反兼容性，因为所提供的操作的输出可能会被请求者简单地忽略。为了确定签名和合约之间的关系，我们要求每个操作的输入和输出参数都由规则中对应类型这些依赖关系由以下表示：图中的虚线箭头。3 .第三章。现在我们考虑行为兼容性，这相当于检查先决条件和结果的兼容性。前置条件由正应用条件L捕获。 为了成功地执行操作，提供者需要来自请求者的某些输入数据以及某些属性以保持当前状态。在图3的提供者规则中，是关于客户、应该被租用的牵引单元和租用时间段的信息。 请求者必须准备好交付这些数据并保证这些属性。因此，请求者的前置条件必须包含提供者的前置条件，它由从L p到L r的一个发生（形式上是一个图同态）来表示。请求者希望从服务操作的调用中获得一些好处。如果一个操作做的比请求者预期的少，那么它就被认为是无用的。换句话说，所提供的操作的效果必须不小于请求者指定的效果。 也就是说请求者规则必须嵌入在提供者中，就像图1中3 .第三章。例如，操作makeReservv另外创建了一个顶点，其类型为EContract，表示公司和客户之间的协议这个顶点没有出现在请求者契约中，因为请求者的目标是进行预订，而不是签署契约。然而，所提供的操作效果符合客户要求。接下来，我们将提出一个（部分）形式化的直观想法ob-从例子中脱离出来。R. Heckel等人理论计算机科学电子笔记105（2004）3743→R←−∈⟨⟩FG G、、、zH，L，RLKrzR，gg，dL（1） dK（2） dR，，h、、、rrTG TGG，rgD h zH，图四、 类型图和图态射（左）和双推出图（右）。4走向正规化合同匹配可以形式化为图转换规则之间的关系。在本节中，我们定义了两种这样的关系，一种是基于规则的操作解释的语义关系，另一种是为语义关系提供充分条件的句法关系然而，首先，我们回顾了图变换的双推出（DPO）[4]方法（参见[3]的调查）和双拉回（DPB）方法[7]的一些基本概念4.1图变换的双推出方法给定一个图TG，称之为类型图，一个TG型（实例）图由图G和类型同态g组成：GTG（cf.图4左侧）与G的每个顶点和边x相关联，其类型g（x）=t在TG中。在这种情况下，我们也写x：t∈G。两个TG型实例图<$G，g <$与<$H，h <$之间的TG型图态射是一个保持类型的图态射f：G→H，即h<$f= g.图变换的DPO方法最初是为顶点和边标记图开发的[4]。在这里，我们提出了打印版本[2]。根据DPO方法，图变换规则，也称为图产生，由内射图态射对（L<$l-K−→R），称为规则跨度。 左侧L包含的项目，必须存在于规则的应用中，右侧R是之后存在的，上下文图K指定了在应用程序中读取但未使用的对象定义4.1（规则，图形转换系统）在TG上，在短TG型规则跨度中，s=（LlK内射TG型图态射R）是一个跨度，图变换系统GT S=TG，P，π由一个类型图TG、一组规则名P和与每个规则名相关联的映射π组成p是TG型规则spanπ（p）. 如果p P是一个规则名，π（p）=s，我们说p：s是GT S。一个具有正应用条件p的语法变换规则是一对R、−→44R. Heckel等人理论计算机科学电子笔记105（2004）37提供提供提供lr储备ri：RentalInfo ri：RentalInfo ri：RentalInfoLKmy_car：February2009RDL（DK（DR提供提供GHcar1：CarGDID=“VWMultivan01”car1：Carpick-upDate=18.12.03returnDate=11.01.04location=“Paderborn”ri1：RentalInfo名称=“ibm”c1：客户ID=“VWMultivan01”pick-upDate=18.12.03returnDate=11.01.04location=“Paderborn”ri1：RentalInfo名称=“ibm”c1：客户cus：客户cus：客户cus：客户my_car：Februarymy_car：February→Lp\\c1：客户提供名称=“ibm”储集 esri1：RentalInfopick-upDate=18.12.03returnDate=11.01.04location=“Paderborn”汽车1：汽车HID=“VWMultivan01”图五、 使用规则reservCar（cus，may car，ri）的DPO图变换步骤。（p，L<$），其中p：s是图变换规则，s=（L<$l−K−→rR）且L是T G-型图，使得L是L的一个子图，且L：LL是相应的包含图（cf.图6左侧）。图中给出了具有积极应用条件的规则的两个例子3 .第三章。图的变换由一对推出图定义，即所谓的双推出构造。定义4.2（DPO图变换）双推出（DPO）图d是如图4右边的图，其中（1）和（2）是推出。给定类型图TG和规则p：s，其中s=（L←−K−→（R）Thep/d从G到H的对应（DPO）变换步骤由G= H表示H，或者简单地G=H，如果图d被理解的话。图3给出了所需操作reservCar（图3）的合同规则的跨度表示及其在实例图中的应用。五、从操作上讲，这一规则的适用过程如下。给定左手边L在G中的出现dL，该应用由两个步骤组成：移除G中与L 1（K）匹配的元素，这不会改变图5中的图G。然后，将R r（K）匹配的元素加到D上，得到的导出图H又含有保留边.将图L和D粘在它们的公共部分K上再次产生给定的图G，即，D是一个所谓的推出补数，左边的平方（1）是一个推出平方。只有在这种情况下，才允许申请。类似地，导出图H是D和R在K上的粘合，其形成RR. Heckel等人理论计算机科学电子笔记105（2004）3745LR⇒\\右手边推出正方形（2）。这种形式化意味着只有保留的顶点可以合并或连接到上下文中的边它反映在DPO方法的识别和悬挂条件中，其特征在于，给定一个规则p：s=（L<$−K−→R），以及左手边，推出补数（1）的存在，因此，p/d变换步骤G=H。标识条件声明对象只有当它们也属于接口时（因此被保留），才可以通过匹配来识别悬挂条件确保通过从G中移除所有要被删除的对象而获得的结构D确实是一个图，也就是说，没有边在没有源节点或目标节点的情况下被留下这种构造确保了给定图H的变化恰好是然而，操作合同代表的操作规范通常是不完整的，也就是说，在转换中应该允许额外的影响。 因此，一个更自由的概念规则的应用是必需的，这确保了至少G与Ll（K）匹配的元素被移除，并且至少与Rr（K）匹配的元素被添加。这种规则解释由图转换的双回调（DPB）方法支持[7]。4.2图变换的双拉回方法已经提出了图转换以提供对图转换规则的更宽松的解释。双回调（DPB）方法引入了图转换，并通过允许额外的更改（未在规则中编码）来推广DPO。图转换是通过用双拉回（DPB）替换转换步骤的双推出图来定义的。定义4.3（图转换）设p：s是规则跨度，其中s=（L←l−K−→rR）。 然后，通过p从G到H的图过渡，表示为p/dG~H，是类似于图6的右边部分的图，其中（1）和（2）都是拉回正方形。一个图的变迁（或brie-y变迁）称为内射，如果g和h都是内射图态射。它被称为忠实的，如果它是单射的，并且态射dL和dR满足以下条件;对所有x，y∈L，y/∈l（K）意味着dL（x）=dL（y），类似地对dR2。一个基于规则规划的G到H的代数变换p/d条件，记为G~H，是通过规则p的图转移，使得2最后一个条件意味着dL和dR满足DPO方法[3]关于l和r的识别条件。46R. Heckel等人理论计算机科学电子笔记105（2004）37勒夫L1R1L2R21←−−→12222111布里尔、、L，RLKr zR，，，dL(1)DK(2)DRdL，，r，G，rgDh zH，见图6。 DPB图过渡与积极的应用条件。存在满足dL=dLl的d L（cf. 图 6在左边）。注意，任何两个给定态射的推出方，使得其中一个是单射的，也是一个拉回方。因此，每个DPO转换也是一个DPB转换。每一个忠实的转换都可以被看作是一个转换步骤加上一个上下文的改变[7]。这是通过在实际步骤之前和之后额外删除和创建元素来建模的。忠实的转换捕捉我们的直觉对合同规范的图形转换规则的松散解释。4.3语义和句法匹配转换的概念允许我们在语义上形式化所需的兼容性概念：提供者和请求者规则在语义上兼容，如果(i)请求者规则的适用性意味着提供者规则的适用性，以及（ii）经由提供者规则的每个转换也可以被认为是经由请求者规则的转换。定义4.4（语义计算）设（p1，L1）和（p2，L2）为具有正应用条件的变换规则，其中s1=（L1←−K−→R）和s=（L<$−K−→R）。我们知道（p，L_∞）是经验的矩阵（p2，L2），在矩阵（p2，L2）中|=match（p1，L<$1），i<$(i) 对于所有的图G，如果t在这里存在dL：L<$1→G，使得dL1：=dL<$◦ 第1章若满足fp1的判别条件，则存在dL2：L2→Gˆ满足dL2：=dL2l1满足p2的定义条件，(ii) 对于所有跨度t：（GgDh（1）如果存在过渡p1/d1p2/d2G~H，则存在一个跃迁G图7）。~H使用相同的底跨t（参见这个定义反映了合约之间的期望关系，但几乎不能应用于确定合约兼容性的算法。因此，我们引入了一种句法匹配关系，它包含了第三节中提出的思想，具有更强的建设性。1R. Heckel等人理论计算机科学电子笔记105（2004）3747hLdL2、2（b）第（1）款，hR，2dR2，、G，，L1R1L2R2→◦112222112勒夫河1升蒸馏水L，rl1Kr1zR，，1，d（一）1L1 1 1(a)HKL1，hLr(3)（4）hL。、、、dL1，l2L2，rKDKzRdR1dL2（二）2，，、r，（aJ）dK21（bJ）L-2，rL第2章G，rgDhzH，见图7。匹配图形转换规则。定义4.5（合成数学）设（p1，L1）和（p2，L2）为具有正应用条件的变换规则，其中s1=（L1←−K−→R）和s=（L<$−K−→R）。我们在战术上有一个t（p，L）syn与（p2，L2）匹配，在系统中（p2：s2，L2）与（p1：s1，L1）匹配，(i) 存在n-内射图同态hL<$：L<$2→L<$1，使得hL{\displaystylel}2满足f {\displaystylep}2的定义条件，(ii) 存在图同态hL：L1→L2，hK：K1→K2和hR：R1R2，使得图（a），（b）和图（c）中的外图都是图同态. 7在左通勤，和图（a）和（b）表示一个忠实的过渡（参见。图7）。在第3节中给出了语法匹配的示例，用于指定所需操作reservCar和所提供操作makeReserve的契约的图转换规则。接下来，我们展示我们方法的合理性。定理4.6（匹配的可靠性）假设两个图变换规则具有正性应用条件p∈1和p∈2。 那么p2匹配p1就意味着p2|=匹配p1。证明（草图）我们表明，def。4.5（一）/（二）需要Def.4.4㈠/ ㈡。ˆ ˆ(i)：GivendL1：L1→G，得到dL：L2→GbydL◦ hL结果ˆ在图（3）的计算中。态射dL2=dL<$2<$l2满足p2的识别条件，因为这个交换性和事实，hL2满足p 2的定义条件。此外，我们可以显示，其余的图在图。7.左为左，右为右。前提条件和结果的相容性条件。(ii)我们必须证明，对于通过第二规则的每个忠实转换，都有通过第一规则的忠实转换。通过假设，在第一规则和第二规则（hL，hK，hR）之间存在图同态，形成忠实的转移（参见图7在右边）。现在，这两种转换都可以是D 1DL、2148R. Heckel等人理论计算机科学电子笔记105（2004）37使用基础拉回正方形的合成垂直合成，并且合成过渡的忠实性来自于dL1的识别条件遵循hL和dL2的识别条件的事实，并且对于右侧类似。Q句法匹配的完整性要求在语义层面上有一个更精细的关系，在陈述（i）和（ii）之间建立一个联系，我们还没有完全解决这个问题。最后一节总结了主要结果，并讨论了更多的开放性问题。5结论在本文中，我们已经开发了正式的概念，基于UML的方法，以服务规范匹配的基础上，图转换规则建模操作合同。我们使用基于DPB图转换的规则的松散解释来获得合同的操作理解和相应的语义匹配关系，并且我们建立了为语义匹配关系提供充分条件的句法关系。今后的工作仍需解决若干问题。一个合理而完整的句法匹配关系需要对语义关系进行细化，并对前置条件和宾语之间的相容性进行约束。正式表示需要扩展到具有属性[8]和子类型[1]的类型化图，这些属性和子类型已经在示例中非正式地使用。在我们的工作中提出的理论概念的实际应用规定通过找到一个足够的XML表示的合同，和工具支持计算的语法匹配关系。引用[1] R.巴尔多赫Ehrig，J. de Lara，O. Runge，G.坦策和我。 温霍尔德 类型化图转换的节点类型继承概念。Fachberichte Informatik 2003-19，柏林技术大学，2003年。[2] A.科拉迪尼Montanari和F.罗西图形处理。Fundamenta Informaticae，26（3，4）：241[3] A. 科拉迪尼 Mo ntanari，F. Rossi，H. 埃赫里克河 He ck el，andM. Léow e.图变换的代数方法，第一部分：基本概念和双推出方法。在G. Rozenberg ， 编 辑 ， Handbook of GraphGrammarsand Computing byGraphTransformation，第1卷：基础，第163-245页。世界科学，1997年。预印本可作为技术。Rep.96/17，Univ. of Pisa，http://www.di.unipi.it/TR/TRengl.html.[4] H. Ehrig，M. Pfender和H.J. Schneider。图文法：代数方法。在第14届IEEE交换和自动机理论年会上，第167-180页。IEEE，1973年。[5] D. Fensel和C.巴斯勒Web服务建模框架。2003年。R. Heckel等人理论计算机科学电子笔记105（2004）3749[6] G. 慌乱。使用WebSphere V5 工具和 技术进行 Web 服务开发和部署第 2 部分：在WebSphereRegistry中发布和查找Web服务。2003.http://www7b.software.ibm.com/wsdd/library/techarticles/0302flurry/flurry2.html。[7] R. Heckel，H.埃里希大学Wolter和A.科拉迪尼图转换系统的双拉回转换与共代数松散语义。Applied Categorical Structures ， 9 （ 1 ） ， 2001 年 1 月 。 另 见 TR 97-07 ， 见http://www.cs.tu-berlin.de/cs/ifb/TechnBerichteListe.html。[8] R. He ck el，J. Küster和G. 泰泽。属性图变换系统的收敛性以. Corradini和H.- J. Kreowski，编辑，Proc.1st Int.Conference on Graph Transformation（ICGT 02），Barcelona，Spain，Lecture Notes in Comp.Science。Springer-Verlag，2002年10月。[9] H. 克里格Web 服务概念架构（WSCA 1.0 ），2001 年5 月。http://www-3.ibm的网站。com/software/solutions/webservices/pdf/WSCA.pdf。[10] S. Narayanan和S.A.麦克莱斯Web服务的模拟、验证和自动组合。第十一届万维网国际会议论文集，第77-88页，檀香山，夏威夷，2002年Press.[11] C.帕尔软件构件匹配本体。In M. Pezze，编辑，软件工程的基本方法：第六届国际会议，FASE2003，LNCS第2621卷，第6-21页Springer，2003年。[12] 我是A.M. Zaremski 签名和规格匹配。博士论文，卡内基梅隆大学，宾夕法尼亚州，1996年1