基于同步网的BPEL建模和验证  

Modeling and Verifying BPEL Using Synchronized Net

作　　者：徐春香[1,2] 屈婉玲[1,2] 王捍贫[1,2] 黄雨[1,2] 袁崇义[1,2] 

机构地区：[1]北京大学信息科学技术学院软件研究所 [2]教育部高可信软件技术重点实验室,北京100871

出　　处：《系统仿真学报》2007年第A01期97-100,共4页Journal of System Simulation

基　　金：973项目(2002CB312004);863项目(2006AA01Z160)。

摘　　要：Web服务组合是面向服务架构的一个应用,是指将已有的Web服务组合成为新的服务。业务流程执行语言BPEL(Business Process Execution Language)是一种描述Web服务组合的语言。为了保证BPEL描述的Web服务组合的正确性,提出了分层建模和验证的思想,将BPEL流程分为逻辑层和语义层,并分别建立形式化模型和验证方法。这样不仅能保证对流程正确地建模,而且能降低建模和验证的复杂度。在逻辑层,BPEL元素映射为基于同步网的WSL_net模型。畅通性和无冗余变迁性质保证了BPEL流程基本控制流的正确性并避免了资源的浪费。语义层的建模和验证将另文给出。Web Service composition is an application of the Service-Oriented Architecture, which refers to combining existing Web Services to a new one. BPEL （Business Process Execution Language） is a language describing the composition of Web Services. The process of composing is error-prone. In order to guarantee the correctness of service composing, the idea of modeling and verifying BPEL in separate levels- the logic level and the semantic level- is proposed. This can not only assure modeling the processes properly, but also lower the complexity of models and verifications. In the logic level, Elements of BPEL, according to the mapping rules, are mapped to WSL_net, which is based on Synchronized Net. Properties such as throughness and no-redundant-transition guarantee the correctness of the basic control flows in BPEL process and avoid unnecessary resource consuming. The modeling and verifying of the semantic level will be given in later papers.

关 键 词：WEB服务组合 BPEL 建模 验证 同步网 WSL_net 

分 类 号：TP391.9[自动化与计算机技术—计算机应用技术]