BPEL与EventB在Web服务组合中的应用与转化

### BPEL与Event B在Web服务组合中的应用与转化 #### 1. BPEL语言基础 BPEL（Business Process Execution Language）语言提供了两类活动： - **基本活动**：代表流程执行的原始操作，包括invoke、receive、reply、assign、terminate、wait和empty活动。 - **结构化活动**：通过使用sequence、if、while和repeat Until等组合运算符，将原始活动和/或其他结构化活动组合而成，用于建模传统控制结构。另外还有pick运算符（基于外部事件定义非确定性选择）和flow运算符（定义嵌套活动的并发执行）。 BPEL还具有以下特点： - 提供异常和故障处理机制，支持在异常发生或合作伙伴请求撤销时，对工作单元内的单个或复合活动进行补偿。 - 能够描述两种类型的流程：可执行流程和抽象流程。可执行流程可以用编程语言实现并由编排器执行，描述服务编排的期望行为；抽象流程代表BPEL流程的视图，隐藏实现细节，不可执行。 - 每个BPEL流程的描述都有对应的XML表示，也有图形表示，并且有多个图形编辑器可用于设计BPEL流程。 #### 2. BPEL与Event B语义 BPEL定义了一种基于流程与其合作伙伴之间交互来描述业务流程行为的语言，用于协调与合作伙伴的多个服务交互。 Event B模型编码了一个状态转换系统，其中变量表示状态，事件表示从一个状态到另一个状态的转换。Event B的细化能力允许从抽象级别逐步引入更多设计决策。其模型的事件是原子事件，通过交错定义事件轨迹，语义是基于交错的轨迹语义。 我们使用Event B对BPEL进行形式化建模的方法，是基于将BPEL定义解释为解释流程协调的转换系统。在BPEL和Event B中，状态都由变量元素表示，BPEL的各种活动对应Event B的EVENTS子句中的事件。 #### 3. 案例研究 - 采购订单流程 以电子 commerce 中的采购订单处理服务为例，当收到客户的采购订单后，流程会同时启动三条路径：计算订单最终价格、选择托运人、安排订单的生产和发货。这三条路径之间存在控制和数据依赖关系，例如计算最终价格需要运费信息，完整的履行计划需要发货日期。当三条并发路径完成后，进行发票处理并将发票发送给客户。 在设计与此案例对应的Web服务组合时，图形编辑器工具提供了两种设计能力： - **一次性Web服务组合描述**：设计人员在单个图形图中生成整个服务组合。 - **逐步Web服务组合设计**：设计人员使用图形BPEL编辑器提供的分解运算符，逐步引入更具体的服务来组成更抽象的服务。 #### 4. BPEL设计到Event B模型的水平转换 将BPEL设计转换为Event B模型的水平转换过程包括静态和动态两部分，由BPEL2B工具支持。 - **静态部分**：将WSDL定义（描述各种Web服务、其数据类型、消息和端口类型）转换为Event B提供的不同数据类型和函数，编码在Event B模型的CONTEXT部分。规则如下： - WSDL消息元素形式化为抽象集，消息的每个部分属性由从消息类型到部分类型的功能关系表示。 - 端口类型的每个操作由从输入消息类型到输出消息类型的功能关系表示。 例如，对于以下WSDL消息和操作定义： ```xml <wsdl:message name="POMessage"> <wsdl:part name="customerInfo" type="sns:customerInfoType"/> <wsdl:part name="purchaseOrder" type="sns:purchaseOrderType"/> </wsdl:message> <wsdl:message name="InvMessage"> <wsdl:part name="IVC" type="sns:InvoiceType" /> </wsdl:message> <wsdl:operation name="sendPurchaseOrder"> <wsdl:input message="pos:POMessage"/> <wsdl:output message="pos:InvMessage"/> </wsdl:operation> ``` 对应的Event B CONTEXT表示如下： ```plaintext SETS POMessage InvMessage CONSTANTS customerInfo purchaseOrder IVCOfInvMessage sendPurchaseOrder AXIOMS axm1 : customerInfo ∈POMessage →customerInfoType axm2 : purchaseOrder ∈POMessage →purchaseOrderType axm4 : IVCOfInvMessage ∈InvMessage →InvoiceType axm15 : sendPurchaseOrder ∈POMessage →InvMessage ``` - **动态部分**：描述BPEL描述中活动的编排过程，形式化为B事件，编码在Event B模型的MACHINE部分。规则如下： - BPEL变量元素由Event B MACHINE的VARIABLES子句中的变量表示，并在INVARIANTS子句中使用messageType属性进行类型定义。 - 每个BPEL简单活动由Event B MACHINE的EVENTS子句中的单个事件表示。 - 每个BPEL结构化活动由编码其组合运算符的Event B描述建模。 例如，对于BPEL变量定义： ```xml <variables> <variable name="PO" messageType="POMessage"/> <variable name="Invoice" messageType="InvMessage"/> <variable name="shippingRequest" messageType="shippingRequestMessage"/> <variable name="shippingInfo" messageType="shippingInfoMessage"/> <variable name="shippingSchedule" messageType="scheduleMessage"/> </variables> ``` 对应的Event B MACHINE的VARIABLES和INVARIANTS部分如下： ```plaintext VARIABLES PO Invoice shippingRequest shippingInfo shippingSchedule INVARIANTS inv1 : PO ⊆POMessage inv2 : card(PO) ≤1 inv3 : Invoice ⊆InvMessage inv4 : card(Invoice) ≤1 inv5 : shippingRequest ⊆ShippingRequestMessage inv6 : card(shippingRequest) ≤1 inv7 : shippingInfo ⊆ShippingInfoMessage inv8 : card(shippingInfo) ≤1 inv9 : shippingSchedule ⊆ScheduleMessage inv10 : card(shippingSchedule) ≤1 ``` 以下是一个结构化活动Compute Price及其对应的Event B表示示例： ```xml <sequence name="Compute Price"> <invoke name="Initiate Price Calculation" partnerLink="invoicing" portType="lns:computePricePT" operation="initiatePriceCalculation" inputVari ```