Web服务编排语言研究："BPEL4WS语言核心语法和语义的定义及关联性概念的探讨

理论计算机科学电子笔记105（2004）51-71www.elsevier.com/locate/entcs走向解释语言Mirko Virolia，1aDEIS，Universit`adegliStudidiBolognaviaVenezia 52，47023 Cesena（FC），Italy摘要我们介绍了一个正式的框架，用于研究Web服务的编排语言的语义。以BPEL4WS语言作为参考案例研究，我们定义了一种核心语言的语法和语义，以从BPEL4WS规范中派生出业务流程的交互行为。这是通过开发一个进程代数来实现的，除了用于选择、顺序和并行组合的通常运算符之外，进程代数还具有命令式编程语言的构造，例如迭代循环和变量赋值。这些都旨在关注相关性的概念，BPEL4WS利用相关性将业务流程定义为多个流程实例的并发行为。关键词：演示语言，Web服务，进程代数。1介绍Web Services技术的研究热点之一是orchestration语言。演示语言指定了现有Web服务之间交互发生时的关系和约束：产生的行为称为业务流程。然后可以开发演示引擎，它采用规范并自动实现实现业务流程的新Web服务。依靠编排语言被认为可以以更一致和更健壮的方式支持复杂服务的开发[16，20]，简化其分析，设计和部署。一些编排语言作为标准化的建议出现1电子邮件地址：mviroli@deis.unibo.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.05.00852M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51Web服务技术中的标准化，例如由包括Microsoft、IBM、IBM System、IBM和SAP [21]的联盟开发的BPEL4WS（用于Web服务的业务流程执行语言），以 及 由 Sun Microsystems 、 Intalio 、 Sterling Commerce 和 CSC [2] 开 发 的BPML（业务流程管理语言）。Web服务编排的概念通常与Web服务编排：由于编排更关注不同Web服务的协调，因此编排是关于单个Web服务或业务流程公开的交互协议。然而，这两个概念并不完全不同。例如，BPEL 4 WS既可以用来描述编排问题，也可以用来描述编排问题;从定义抽象流程的核心部分开始，引入了两个小的扩展来处理可执行流程建模编排问题，以及业务协议建模编排问题。另一方面，BPML只处理编排问题，它建立在WSCI的编排标准之上[3]。由于我们认识到这两个概念之间的紧密关系和重叠，因此在本文中，我们选择BPEL 4 WS（有时简称BPEL 4 WS）作为研究Web服务组织概念的案例研究-尽管目前还不清楚这两个概念中的哪一个将真正成为标准。然而，我们相信我们的研究和方法的重要部分也可以应用于BPML，其细节留给未来的研究。在许多现有的松散耦合的Web服务之上-可能由不同的供应商实现并驻留在不同的组织中- 然后使用编排语言来从它们中指定完整的、健壮的和一致的业务流程特别是，这样的语言是为了定义Web服务协调现有活动的行为，通过强制利用给定的交互协议，支持不同的工作会话-也称为流程实例-，支持长时间运行的事务，提供管理异常的设施，等等。从软件工程的角度来看，编排Web服务的一般任务并不新鲜，但传统上被称为协调活动[9，13，19] -即，统治和管理不同软件组件的交互。自从原型协调语言Linda引入以来，许多现有的协调模型已经被研究和工程化[12] - JavaSpaces [11]、TuCSoN [22]、KLAIM [10]和Manifold [1]，其中一些特性和思想实际上被编排语言所借鉴。一般来说，协调任务在业务场景中是一个特别重要的任务，因为它意味着包括使一组不同的M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5153软件组件成为一个完整的系统--一个可靠有效地服务于其预期目的的工程制品因此，协调模型和语言已经成为一个彻底的正式研究的主题并不奇怪，其目标是精确描述它们的语义，证明它们的属性，并推动正确和有效实现的发展。重要的例子是Linda的过程代数方法[6]，以及[23]的协调服务的正式框架。大多数现有的作品在这个方向上依赖于进程代数技术，因为它们提供了一个方便的框架，正式协调模型，其内在的能力来处理的概念，互动和并发行为。类似的方法也适用于编排语言[16，15]，其主要目标是改进现有的规范，- 正如任何其他散文文档一样-有时可能是模棱两可的，在相关方面过于紧凑和/或在不太有趣的方面过于冗长。尽管如此，在为编排语言（如ORM）提供形式化模型的过程中，人们注意到进程代数确实被认为是一个参考，但也增加了一些新的和有趣的问题，值得研究。最值得注意的是，除了用于发送和接收消息以及以并发、排他或顺序方式组成活动的典型流程代数运算符之外，还引入了命令式结构，因此，本文的目标是研究所有这些结构之间的关系，提供一个正式的帐户的意义规范和相应的业务流程的行为。这是通过引入一种BPEL4WS核心语言来实现的，该语言专注于其功能的严格子集，并正式描述其（抽象）语法和操作语义。本研究的目的不是研究由非线性引入的某些特征的正常性质，例如[7，5]。相反，遵循主流技术的其他核心语言背后的直觉-轻量级Java [14]是一个显著的例子-我们的目标隔离语言的一个子集，提供其语义的精确、正式的描述。特别是，在本文中，我们确定的新机制，是值得研究的相关性，因为它是一个业务流程和流程实例之间的关系的核心，整个编排的想法。因此，这种核心语言可以作为一种描述工具，完成对特定对象的描述，避免歧义和欠规范，并使属性的正式研究成为可能-例如，类型问题或行为方面。此外，它还可以作为可拓学研究54M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51BPEL4WS的其他特性（如补偿和故障处理程序），或者添加新机制的建议。本文其余部分的组织如下。第2节简要描述了BPEL4WS编排语言，介绍了一个用于处理物品运输的业务流程的经典示例，该示例贯穿全文，作为案例研究来展示模型的细节。第3节解释了我们的正式模型的目标和范围，介绍了我们使用的抽象语法来代替真正的语法规范。第4节为核心语言提供了操作语义，考虑了业务流程的必要执行方面，包括流程实例和可变分配。最后，第五节提供了结论性意见，并讨论了未来的工作前景。2使用业务流程语言进行2.1BPEL4WSBPEL 4WS是一种基于XML的规范语言，用于描述编排不同的、现有的和可能动态出现的Web服务的交互的业务流程。因此，它建立在WSDL语言之上，用于描述Web服务的接口[8]。这在端口类型、动作和消息方面进行了在面向对象的特别是，就JavaScript而言，动作可以有两种交互行为：单向，当它们被异步调用而不等待任何应答时，或者请求-应答，在实际期望应答的情况下。BPEL4WS规范由四个声明部分组成：伙伴链接、变量、相关集和实现业务流程的活动伙伴链接通过指定流程/Web服务和Web服务/流程交互的端口类型，标识业务流程与其他Web服务交互的关系。值得注意的是，编排语言从不直接引用特定安装的Web服务，而是引用通用端口类型，这些端口类型将在部署时绑定，甚至在运行时动态绑定。这种抽象是特别相关的，因为它还支持那些根据负载平衡问题将Web服务池动态绑定和解除绑定到业务流程业务流程的关键思想是，它的全局任务被划分为不同的会话，称为流程实例，每个会话负责执行M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5155为每个用户提供单独的服务或工作-无论这是人还是另一个服务。为了支持这种情况，可以定义变量，这些变量可以携带XML数据值和消息，并用于定义每个流程实例的状态。最值得注意的是，变量也可以包含伙伴链接，即对其他服务的抽象引用：类似于π-演算，其中通道用于交换通道名称[18]，这种机制有助于表达动态互连结构。然后引入相关集来识别与给定流程实例相关的那些交互，这对于在各种并发会话之间正确地分派消息是必要的。每个关联集都是一组属性，它们是部分消息的别名，并且被类似于一次写入变量处理：在给定时间，对于每个流程实例，许多关联集都是活动的，并且与所有属性相关联的值唯一地标识流程实例。例如，与给定客户请求相关的所有消息最后，指定一个活动来描述业务流程的精确行为。活动通常是通过结构化活动组合基本活动来构建的。基本活动包括发送和接收请求和应答（调用、接收和应答）的行为，这些行为可以指定它们必须遵守的一个或多个现有相关集，或者新的相关集。要初始化的关系集。在其他基本活动中，有可变分配（assign），通过私有链接（源和目标）同步内部并发活动，等待超时（wait）和引发错误（throw）。结构化活动实现了顺序组合（sequence）、保护选择（pick）、并行组合（flow）、迭代周期（while）和多个用例（switch）。2.2为例作为一个参考案例研究，在本文中，我们考虑BPEL4WS [21]（第16.1节）的业务规范中描述的航运服务。尽管这个例子很简单，但它涵盖了我们感兴趣的大多数语言特性，包括相关集、变量和流控制结构。这个例子描述了一个Web服务，它实现了一个处理客户所请求的订单的服务，这些订单本身被建模为Web服务。处理两种类型的发货：客户可能要求以原子方式发货，在这种情况下，会向客户发送一个发货通知回调;或者客户可能指定一个未完成的订单，在这种情况下，将在不同阶段发货，每个阶段发送一个不同的发货通知。时间56M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51按照上一节中介绍的模式，该规范定义了合作伙伴链接、变量、相关集和业务活动。这里只指定了一个合作伙伴链接来表示客户服务：客户通过名为shippingRequest的单向请求调用服务，服务通过名为shippingNotice的操作执行对客户的单向调用来提供通知。发货请求消息由三个部分：一个orderID整数，一个完整的布尔值，指定是否请求是否被原子地处理，以及一个itemsTotal整数，表示要发送的项目数。 发货通知消息由orderID整数和itemsCount整数组成，表示当前发货的项目数。在这个业务过程中使用了三个变量：shipRequest用于存储接收到的消息，shipNotice用于存储要发送的消息，itemsShipped用于计算已经发送的物品数量。只定义了一个包含prop-orderID的相关集：流程实例的唯一特征是相同的命令标识符。最后，实现业务流程的活动如图1所示。在这里，带下划线的部分并不表示实际的XML代码，而是非正式地描述更复杂的XML代码的占位符，为了简洁起见，没有报告其细节。实现的算法如下。当收到请求时，如果如果其完整部分为true，则立即使用相同的itemsCount调用应答。否则，执行while迭代。每次，shipNotice消息的itemsCount部分都被分配给特殊的标识符opaque，这意味着分配的结果是不确定的- 建模，例如与一些后端服务的交互，其不与模型交互。相应地，向客户发送消息，通知运送的物品的数量。当这个数字达到客户请求的总金额时，流程实例终止。 特别是所有指定的调用和接收活动链接到相关集，以便携带相同orderID的交互绑定到相同的流程实例，表示与客户的工作会话。3BPEL4WS的正式规范在本文中，我们为遵循BPEL 4WS规范的编排服务的行为引入了一个正式模型，为现有的非正式规范提供了一个正式的解释[21]。BPEL4WS实际上具有一组相对较大且异构的结构、机制和细节：提供完整的形式化超出了本文的范围。相反，按照编程语言[14，6]背景下的通常研究方法，我们发现M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5157<接收shipRequest>.联系我们<开关><案例shipRequest.shipComplete>shipNotice.item sCo un t：= sh ipR eq ue st. it ems Count<调用shipNotice>./invoke><产品展示<否则> itemsShipped：=0/assign><而条件=itemsShipRequest.itemsTotal> shipNotice.itemsCount：=opaque/assign><调用shipNotice>./invoke>itemsShipped+=sh ip No t ic e. ite ms Co untFig. 1.运输服务专注于语言的较小但重要的子集是有用的， 一个核心语言感兴趣的特征。3.1模型选择我们这里的目标是研究过程实例的概念，即单个业务过程实际上由不同的子过程组成这一方面，在相关集和变量分配的机制中，是整个编排方法的基础，因此值得仔细研究。此外，这样的研究使我们有机会加深58M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51进程代数方法的典型编程构造（例如并行组合和选择）、命令式语言的其它编程构造（变量及其赋值）以及通过相关集引入的对进程实例的因此，我们的核心语言有意忽略了一些有趣的方面，如超时、错误处理程序、补偿处理程序、伙伴链接的可重构性、XML数据表示等，包括这些机制与我们在这里感兴趣的研究方面的结束无关;相反，它们可以稍后以一种基本上正交的方式在我们的语言之上引入，以便提供对BPEL 4 WS的完整的正式说明。从语法上讲，我们介绍的语言是BPEL4WS子集的抽象版本：尽管大多数结构都有到核心语言的一对一转换，但有时映射需要一些辅助工作，为了处理简单，这些工作只是非正式地描述。操作语义遵循进程代数上的标记转移系统的标准方法，描述了一个行为规范如何随着内部计算或与环境的交互发生而移动到另一个行为规范。遵循BPEL 4WS在描述伙伴链接时使用的抽象，我们不描述与其他Web服务的交互细节以及相关属性，如同步性、直接性、传输协议等。相反，任何交互的特征在于（i）其含义（调用/应答），（ii）其方向（由业务流程发送或接收），（iii）所涉及的对等体（伙伴链接），以及（iv）内容（携带的消息）。我们介绍的语言没有配备必要的附加形式结构来检查规范的语义正确性，例如，验证变量在初始化之前被使用，相关集没有被初始化两次，等等。由于这将导致一个非常显着的建模工具，其对Web服务技术的重要性在[16]中讨论过，所以这里没有分析它，因为它可能是我们未来研究的主题。因此，我们也避免考虑规范中处理属性、变量、相关集、端口类型等声明的部分，而是关注它们的利用以及它们对业务流程运行时行为的影响。3.2抽象语法设u是整数和布尔值的元变量，v是变量（所有值），p是属性（形成相关集）。Meta-变量l的范围覆盖端点，端点在概念上可以看作是伙伴链接、动作名称和方向的三元组：它们唯一地标识M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5159w：：=v|p变量和属性e：：=不透明|u|v|f（e）表达式s：：= 0|send（l，v，w）|recv（l，v，w）|while（e）{a}|switch（e）{a：a}|空规格发送消息接收消息迭代结构交换结构变量赋值源（λ）|目标值（λ）|内部链接操作a; a|（a）|a + a序列、并行组合和选择a：：=s活动图二. 抽象语法一种互动发生的渠道。给定任何元变量x，我们让x在x个元素的序列上范围（例如，x1，x2，. ，x k）;相应地，x i是一个这样的序列的第i个元素，x∈x用于声明x=xi对于某个i，符号·用于空序列。我们介绍的语言的语法如图2所示。请注意，虽然类似于非常知名的过程代数运算符的结构化活动由标准理论符号表示，但我们对其他活动使用了类似于XML语言的抽象语法。元变量w涵盖变量和属性：它们的赋值定义了给定流程实例的当前状态。这里的表达式可以是不透明的标识符，它在赋值时可以非确定性地假设任何值，布尔值或整数值，变量，或者通过一些数学函数或运算符f的表达式组合。例如，我们允许表达式+（v，1）-也写为为了清楚起见，使用整数表示法v+ 1-代表与v和1相关的值之和，类似地写为例如v >10，v≥vJ，v+5 = 8等等。图3描述了活动的具体XML语法与抽象语法的关系。在左侧，我们使用x表示描述相应右侧元变量x的XML表示-例如，a 160M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51a 1. a n作为1; ; an a 1. a n/流量>作为一个1…an onMessagea M1>a 1/onMessage>... a k/onMessage>/pick>作为一个M;一个1+...+ aM; ak1Ka/while>如（e）{a}<开关>a 1/case> a 2.如switch（e1）{a1：switch（e2）{a2：作为源（λ）作为目标（λ） from expr.= e> to variable=v>/assign> asassign（v，e）<调用lv> corr.>公司简介/invoke>assend（l，v，w）<接收lv> corr.>公司简介联系我们作为recv（l，v，w） corr.> 公司简介/reply>assend（l，v，w）<联系我们 w inw out/corr.>send（i，i，i）;recv（l，vout，wout）图三. 具体语法到抽象语法代表右侧符号a1，它定义了一个活动。结构化活动序列和流程分别映射到标准二元运算符“;”和““的连续应用，类似地，pick映射到choice运算符+，由每个不同选择的消息交换的发生来保护。活动while、link、source和assign具有一对一的映射，而M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5161开关对应于单情况构造开关的连续应用。activityinvoke和reply用于发送调用或回复，并映射到相同的结构send-它们的差异旨在记录到两个端点l中，它们具有相反的方向。相反，活动receive被映射到构造recv。最后，由于指定输入和输出消息的调用引用请求-应答原语，它被映射到发送和接收的序列。唯一需要更准确描述的部分应该是相关性的人，这导致了与消息交换发送和接收相关的活动中的额外参数w。 作为第一个例子，考虑一个没有相关性的简单调用，发送一个给定的结构化消息。 不失一般性，在我们的抽象语法中，我们总是把消息看作是由一系列值组成的，因此我们用v表示一个保存消息的变量，用v i表示它的第i个子部分（或字段）上的相应变量。例如，没有相关性<援引...输入变量=varName>表示为send（l，vvarName，vvarName）。第一个参数是消息接收者端点，第二个是将包含接收到的消息的变量，而第三个包含相关性的信息：当不存在相关性时，这与第二个参数完全相同。现在假设消息的类型为msg，它由三个部分组成：part1、part2和part3，它由变量v=v1，v2，v3表示，并假设在调用活动中指定了以下相关性集< correlation set=cName.> 相 关 <性>根据定义我们将cName定义为由属性p1和p2组成的相关集，它们链接到消息msg的第一部分和第二部分。这个关联集将在msg消息的第一部分和第二部分中使用给定的值来标识那些交换消息的流程实例相应的抽象语法现在是send（l，v1，v2，v3n，vp1，p2，v3n）。特别是第三个论点p1，p2，v3表示消息的第三部分与任何相关集无关，因为它是变量v3，而前两部分是属性p162M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51recev（lr，vr，vrp，vr，vrp）;2 3switch（vr）{assign（vn，vr）;send（ln，vn，vip，vn）：22 32return（vi，0）;while（vi vr）{return（vn，opaque）;32send（ln，vn，nn，n）;2（vi，vi+vn）}}2见图4。运输服务和p2，然后与流程实例相关。因此，如果在当前流程实例中，p1绑定到值u1，p2绑定到值u2，那么消息的第一部分和第二部分将自动设置为u1和u2。 对偶地，在recv（l，v1，v2，v3n，vp1，p2，v3n）中，只有在第一部分和第二部分中携带u1和u2这就是为什么我们通常将消息发送表示为send（l，v，w），并且对于消息接收也是类似的3.3航运服务的抽象概念为了提供更多关于抽象语法的细节，我们描述了2.2节中所示的shipping服务的规范。使用两个端点：ln表示在客户上调用的actionshippingNotice，lr用于客户调用actionshippingRequest。 符号vr用于变量shipRequest，包含接收到的请求消息，其由三个部分vr、vr和vr1 2 3表示orderID、complete和itemsTotal。符号vn用于变量shipNotice，包含要发送的消息，由两部分vn和vn，表示orderID和itemsCount。 那么，符号vi1 2用于变量itemsShipped。相关集的属性p用于订单ID。然后，可以直接从该规范中获得shipping服务的抽象语法，如图4所示。 从一开始如果你看一眼，读者可能会喜欢它的紧凑性超过实际规格，以及它的直观结构。4语义4.1扩展语法上一节中描述的语法是表层语法，可以用来以抽象的方式描述具体化。另M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5163另一方面，为了提供描述编排Web服务的实际行为的操作语义，我们还需要该语法能够表示给定时间的业务流程的状态。特别是，当前变量赋值和过程实例的概念必须进入画面，因为它们在我们打算定义的模型中起着基本的作用。因此，作为函数式和并发编程语言中的常见做法[14，24]，我们扩展了语法来处理运行时方面。符号a的生产变更如下：a：：= 0|（w›→u）s|！一|aaa在项（w<$→u）s中，记法（w<$→u）被称为存储，用于指定在活动规范s中，变量或属性wi与值ui相关联，对于任何i。在下文中使用符号（w<$→u）（w<$→u），其含义与（w，w<$→u，u）相同。符号！a意味着活动a可以被派生（复制），然后在有限的时间内执行，而操作符CUP则用于组合流程实例。 特别是，当存储被用于对流程实例的当前状态进行建模时（在变量和相关集方面），复制被用于在顶层处理流程实例。注意，我们有两个用于并行组合的操作符：用于组合不同流程实例的CUP和用于组合同一流程实例中不同活动的CUP：它们要保持不同，因为存储不通过CUP传播，但不通过CUP传播。然后计算模型如下：如果s是通过一个递归过程在语法上获得的活动，规格，！（··）s是业务流程的初始状态，每次接收到每个工作会话的第4.2同余规则与辅助算子作为定义操作语义的第一步，我们通过引入图5中报告的同余规则来细化抽象语法，指定那些被认为在语法上等价的术语。这些规则给出了关于复制[C-SPN]、并行组合[C-PAR]、选择[C-FLW]、选择[C-CHO]和顺序组合[C-SEQ]的语义细节，这些规则是从过程代数风格（例如CCS [17]和BPA [4]）中派生出来的。在介绍操作语义之前，我们先阐明存储和变量的管理。变量和属性之间的主要区别是通过引入一个用于建模存储更新的部分操作符来解决的，强制执行属性是常量的思想：64M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51！一个混蛋！aaa（w›→u）0 0[C-SPN]aP0 aPaJa jPaaP（aJPaJJ）（aPaJ）PaJJ[C-PAR]s0 sss js jss（sjsJJ）（ssJ）sJJ[C-FLW]s+0ss+sJsJ+ss+（sJ+sJJ）<$（s+sJ）+sJJ[C-CHO]% s; %0%s % 0;% s %s（s;sJ）;sJJs;（sJ;sJJ）[C-SEQ]图五、结构同余规则关联集的值标识进程标识，它永远不会改变。该运算符定义为：（w<$→u）（v<$→u）（w<$→u）（v<$→u）（w<$→u）（p<$→u）（p<$→u）（w<$→u）（p<$→u）（w<$→u）<$（p<$→u）（w<$→u）（p<$→u）ifp∈/w第一个定义指出变量赋值总是更新存储，第二个和第三个定义指出只有当存储中已经发生等效赋值我们使用这个定义来强化这样一种思想，即给定流程实例发送和接收的消息必须符合相关集，因为例如，当u/=uJ时，符号（p<$→u）n（p<$→uJ）没有意义。为简单起见，存储的表示法被滥用为（w<$→u）<$（wJ<$→uJ）作为（w <$→ u）<$（wJ<$→ uJ）<$（wJ<$→ uJ）<$的简写. （wJ<$→ uJ），其中k是wJ和uJ的大小。1 1 22 k k表达式e在store（w→u）下的求值由符号{w/u}e，带语义：{w/u}uu{w/u}wiui{w/u}f（e）f（{w/u}e）{w/u}opaqueuv∈/w{w/u}vu有序地，值被评估为它们自己，变量和属性被评估为它们的关联值，函数通过将评估传播到它们的参数，不透明标识符或尚未初始化为任何值u的变量（非确定性地）。请注意，求值的符号再次被滥用，使用{w/u}e来计算所有表达式e，并且类似地用于计算整数和布尔表达式。M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5165000000一个联合国aJ−→αaJJPaJ如果a−→αaJJ[PAR]（w<$→u）（s0+s1）−→α（w<$→u）（s0<$s1）−→α（wJ<$→uJ）sJ（wJ<$→uJ）（sJif（w<$→u）s0−→αs1）if（w<$→u）s0−→α（wJ<$→uJ）sJ（wJ<$→uJ）sJ[PCK][FLW]（w<$→u）（s0;s1）−→α（wJ<$→uJ）（sJ;s1） if（w<$→u）s0−→α（wJ<$→uJ）sJ[SEQ]（w<$→u）（source（λ）;starget（λ）;sJ）−→τ（w<$→u）（s<$sJ）[LNK]（w<$→u）while（e）{s}−→τ（w<$→u）while（e）{a}−→τ（w›→u）s;while（e）{s}if{w/u}e =true[WH]（w›→u）0if{w/u}e =false[NWH]（w<$→u）switch（e）{s：sJ}−→τ（w<$→u）switch（e）{s：sJ}−→τ（w›→u）s如果{w/u}e=true[SW]（w›→u）sJif{w/u}e =false[NSW]（w<$→u）assign（v，e）−→τ（w<$→u）（v→ {w/u}e）0 [助理秘书长]l！{w/u}v（w<$→u）send（l，v，wp）−→（w<$→u）<$（wp<$→{w/u}v）0 [SND]我吗？uJ（w<$→u）recv（l，v，wp）−−→（w<$→u）<$（v<$→uJ）（wp<$→uJ）0[REC]见图6。操作语义4.3操作语义与并发语言[17，6，23]一样，操作语义在这里由标记的转换系统定义，其中A是活动的集合（要建模的系统的状态），由元变量a排列，I是表示交互的标签的集合，由语法的元变量αα：：= τ|l！u|我吗？u这个过渡系统用于确定业务的状态如何，cessevolve是与合作伙伴发生的交互，为某个活动编写a−→αAJ66M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）51（状态）a通过相互作用α移动到aJ。τ是无声的动作，在业务流程中建模内部计算;l！u表示向端点l发送消息的业务流程，该消息指定消息u，类似地，l？U表示从端点L接收消息。定义转换关系→的规则如图6所示。规则[PAR]从交错并发的角度定义了操作符PARP的语义，并允许我们从这里开始关注单个M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5167处理（w→u）s类型的实例。规则[PCK，FLW，SEQ]描述了选择，队列和顺序组合的语义：采用了这些操作符的标准代数行为，以及每个转换可能会删除封闭过程实例的存储的想法。同一流程实例中的两个不同的并发活动可以通过源和目标链接λ进行同步，如规则[LNK]所示有了上述规则，我们现在可以一次处理一个其他基本活动的执行，而不需要考虑它们之间的相互影响。结构化活动while通过在当前存储中评估布尔条件e来执行：如果这是真的（[WH]），则首先执行动作s，然后再次执行while活动，否则（[NWH]），不必执行其他本地活动-但例如，顺序继续可以通过规则[SEQ]进行。开关结构的行为是相似的，评估第一种情况，如果满足其条件（[SW]），则执行相应的活动s，否则考虑后续情况（[NSW]）。将表达式e赋值给变量v，意味着通过将v赋值给值u来更新存储，e的值为（[ASG]）。动作send导致一条消息被发送到外部，其内容是当前存储中变量v的求值{w/u}v。因此，应用了udpate（wp<$→ {w/u}v），它既检查消息相对于现有相关集的属性的一致性，又在存储中添加新属性，从而对新相关集的初始化进行建模（[SND]）。反之亦然，通过动作recv接收新消息，使得其内容uJ通过update（v›→uJ）被分配给变量v此外，还应用新的更新（wp> →uJ），其在必要时控制所接收的值是否符合现有属性，并且添加新的相关集的属性。特别是，注意传入消息必须与适当的流程实例相关联，因为它只允许在提供兼容相关集的流程实例4.4航运服务行为为了更好地理解我们的操作语义的主要基础，我们展示了航运服务的演变，这是由于与一些客户的互动。为了简洁起见，我们用sT表示下式所示的规格：68M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）5122232232图4中，由ssw和swh组成的switch和while活动在里面，即：sT：：=recv（lr，vr，vip，vr，vr）;sswssw：：=switch（vr）{assign（vn，vr）;send（ln，vn，vip，vn）：assign（vi，0）;swh}swh：：=while（vi vr）{assign（vn，opaque）;3 2send（ln，vn，nn，n）;return（vi，vi+vn）}作为一个案例，我们考虑以下演变：• 业务流程的初始状态为0=！（· → ·）sT，也就是说，指定sT的任何副本都准备好被派生，其初始存储是无效的。• 在给定的时间，客户发送这样的发货请求101，true，5L R？101，真，5分a0−→a0Pa1，a1=（vr→101，true， 5μ m）（p<$→101）ssw这首先是通过同余规则[C-SPN]生成一个新的流程实例来实现的这个执行的结果是存储将包含接收到的消息的变量vr，而定义流程实例标识的相关集属性p绑定到101。• 并发地，一个新客户发送了一个请求180，false， 3，请求使用ID 180进行3个物品的可能非原子装运;因此，与前面的情况类似地创建了一个新的流程实例L R？180，假，3a0Pa1−→a0Pa1Pa2，a2=（vr<$→180，false， 3）（p<$→180）ssw注意，现在有两个流程实例是活动的，每个实例都有自己的存储状态，其特征是不同的orderID。•1和2的执行是孤立的。不失一般性，因为我们处于交错并发的上下文中，我们可以假设第一个流程实例a1的执行一直进行到完成，即（i）评估切换条件，（ii）分配变量，然后M. Viroli/Electronic Notes in Theoretical Computer Science 105（2004）516912222㈢执行调用：α1−→τ（vr<$→101，true，5）（p<$→101）assign（vn，vr）;send（l，vn，p，vn）−→τ23n 2（v r→ 101，true，5）（p<$→ 101）（v n<$→ 5）; send（l，v r，p，vn<$）ln！101，500美元2n2−−−−−→在最后一次交互中，注意获得了第一个消息部分101通过计算变量vn这是没有初始化：然而，从所有的选择可能性101是因为它是唯一匹配相关集属性p（rule [SND]）的当前值的。• 同样，我们报告了第二个流程实例的演变，它处理3个项目的非原子装运。我们首先假设业务流程发送1个项目：a0Pa0Pα2−→τ（vr→180，false， 3）（p<$→180）assign（vi，0）;swh−→τa0P（vr→180，false， 3）（p<$→180）（vi<$→0）swh−→τa0P（vr →180，false， 3）（p→0）assign（vn，opaque）;send（l，vn，vip，vn）;assign（vi，vi+vn）;s−→τ2n22白色a0P（vr→180，false， 3）（p<$→180）（vi<$→0）（vn<$→1）发送（l ，vn，vnnn）;assign（vi，vi+vn）;sln！180，1美元n2 2wh−→a0P（vr→180，false， 3）（p<$→180）（vi<$→0）（vn<$→1）return（vi，vi+vn）; −→τa0P（vr→180，false， 3）（p<$→180）（vi<$→1）（vn<$→1）swh请注意，在此演变之后，交互状态移回初始状态