基于模块化可达图的服务组合验证及BPEL代码生成

Verifying Service Composition Based on Modular Reachability Graph and Generating BPEL Codes

为了解决基于中介器服务组合方法的状态爆炸和不能自动生成BPEL(business process execution language)的问题,提出了一种基于Petri网模块化可达图的服务组合验证方法.服务组合的Petri网模型通过中介变迁进行模型分割,分别对各个部分构建可达图,再对模块化可达图进行服务组合可行性分析.采用模块化可达图可以大量节省空间开销,有效避免空间爆炸问题.在验证服务组合可行的情况下提出了基于ECA规则形式的BPEL过程代码自动生成方法,也就是将服务组合Petri网模型的中介变迁以及每个服务对外接口的调用或操作都映射生成为ECA规则形式的BPEL代码段.通过对一个电子商务实例进行分析,说明了所提出方法的有效性.

To address state space explosion and the inability to automatically generate the BPEL （business process execution language） codes of the existing methods of composing services based on mediators, this paper presents an approach to verify the Petri net models of service composition by modular reachability graphs. In this approach, the Petri net models of service composition are divided into sub-models in a modular way, and verify the feasibility of composition by analyzing the state spaces of individual sub-models, without unfolding to the ordinary state space. Using this modular technique can avoid the state space explosion. After verification of the feasibility, the paper proposes a method of automatically generating the BPEL codes of the whole composite service from the Petri net models of composition. The main idea is to generate the BEPL codes from the fused transitions between the sub-models based on ECA rules. Finally, an application of the methods is illustrated though a case study in an e-business enterprise.