A Calculus for Generation, Verification and Refinement of BPEL Specifications

Business Process Execution Language for Web Services (WS-BPEL) is the emerging standard for designing Web Services compositions. In this context, formal methods can contribute to increased reliability and consistency in the BPEL design process. In this paper we propose an approach based on the HAL Toolkit that allows verification of the correctness of the behavior of a π-based specification of interacting Web Services, and generates the BPEL processes that have the same behavior. This correlation based on two-way mapping between the π-based orchestration calculus and BPEL. This approach facilitates the verification and refinement process and may be applied to any BPEL implementation.     

A Formal Framework for Web Services Coordination

Recently the term Web Services Choreography has been introduced to address some issues related to Web Services Composition and Coordination. Several proposals for describing Choreography for Business Processes have been presented in the last years and many of these languages (e.g. BPEL4WS) make use of concepts as long-running transactions and compensations for coping with error handling. However, the complexity of BPEL4WS makes it difficult to formally define this framework, thus limiting the formal reasoning about the designed applications. In this paper, we formally address Web Services Coordination with particular attention to Web transactions. We enhance our past work - the Event Calculus - introducing two main novelties: i) a multicast event notification mechanism, and ii) event scope names binding. The former enables an easier specification of complex coordination scenarios — such as E-commerce applications require — while the latter allows many new interesting behaviors which can be very useful in business scenarios: the introduction of private event scope names — used to deal with security and privacy — and a dynamic event scopes definition that can be used to manage multiple instances of the same application.     

A core calculus for correlation in orchestration languages

We introduce a formal framework for studying the mechanism of correlation in orchestration languages for Web Services. A core calculus based on typical process algebraic constructs is developed, enhanced with two mechanisms: (i) a management of scopes keeping track of variables, properties, and their assignment to values, and (ii) a construct to spawn service instances handling (cor-)related operations and guaranteeing consistent routing of messages. By abstracting away from low-level details of orchestration languages, this model can be used as a foundation for the correlation mechanism, paving the way towards the analysis of properties and the design of extensions and improvements. As an example application, we show how the calculus introduced can be extended with few imperative and control-flow constructs reaching the expressiveness of a significant fragment of BPEL orchestration language.     

Web服务组合语言的出错与补偿处理的pi演算编码

本文研究了Web服务组合语言BPEL4WS的出错与补偿处理的pi演算编码,目的是实现Web服务组合语言BPEL4WS自动验证过程。本文对pi演算进行扩充以编码BPEL4WS程序,给出了pi演算对BPEL活动的编码规则。在一个作用域的条件下,用pi演算的通信并发结构表示BPEL4WS规范的出错与补偿处理结构,采用传名机制分别处理程序化显式抛出故障与非程序序化抛出故障的捕获,给出BPEL4WS的出错与补偿处理的pi演算编码,为系统地完成从Web服务组合语言BPEL4WS规范到扩展pi演算的编码奠定了基础。     

Session types for safe Web service orchestration

We address the general problem of interaction safety in Web service orchestrations. By considering an essential subset of the BPEL orchestration language, we define SeB, a session based style of this subset. We discuss the formal semantics of SeB and present its main properties. We take a new approach to address the formal semantics which is based on a translation into so-called control graphs. Our semantics accounts for BPEL control links and addresses the static semantics that prescribes the valid usage of variables. We also provide the semantics of service configurations.During a session, a client and a service can engage in a complex series of interactions. By means of the provided semantics, we define precisely what is meant by interaction safety. We then introduce session types in order to prescribe the correct orderings of these interactions. Service providers must declare their provided and required session types. We define a typing algorithm that checks if a service orchestration behaves according to its declared provided and required types.Using a subtyping relation defined on session types, we show that any configuration of well-typed service partners with compatible session types are interaction safe, i.e., involved partners never receive unexpected messages.     

基于Pi-演算的BPEL4WS Web服务组合形式化模型

Web服务组合研究领域的一个重要的问题是如何形式化描述Web服务组合,如何验证服务组合的正确性。Web服务组合的形式化模型来可以用来检查、验证Web服务组合以保证组合的正确性。Pi-演算是一种适合于Web服务组合建模的进程代数。本文介绍了P-演算的基本语法,针对目前最主要的一种描述和执行基于工作流模式的Web服务组合的规范-Web服务商业流程执行语言（Business Process Execution Language for Web Services,BPEL4WS）,定义了Pi-演算和BPEL4WS之间的概念映射,并给出了BPEL4WS的基于P-演算的形式化模型,最后通过一个案例给出了模型验证的方法。     

基于接口自动机的BPEL4WS Web服务组合形式化模型

介绍了接口自动机的基本语法,针对目前最主要的一种描述和执行基于工作流模式的Web服务组合的规范——Web服务商业流程执行语言 (business process execution language for Web services,BPEL4WS),定义了接口自动机和BPEL4WS之间的概念映射,并给出了BPEL4WS的基于接口自动机的形式化模型,最后通过一个案例给出了BPEL4WS到接口自动机的映射及验证的方法。     

基于翻译模式的BPEL到LOTOS映射方法研究

为了实现由BPEL描述的Web服务组合到LOTOS的自动化转换, 提出一种基于翻译模式的转换算法。从BPEL语言的XML schema定义出发, 分析BPEL本身的语言结构, 得到BPEL语言的产生式。再根据BPEL到LOTOS的语义映射规则, 设计BPEL到LOTOS的翻译模式。同时, 在基本映射规则之上, 给出BPEL到LOTOS的数据类型和故障处理机制的转换规则。最后结合Web服务实例, 验证该工具的可行性。     

Modeling business processes with BPEL4WS

Business Process Execution Language for Web Services (BPEL4WS) allows defining both, business processes that make use of Web services, and business processes that externalize their functionality as Web services. This short paper introduces the basic language elements of BPEL4WS using a simple example. The concepts underlying the language are briefly explained: establishing bilateral partnerships, correlating messages and processes, defining the order of the activities of a business process, event handling, handling exceptions via long-running transactions, and the usage of BPEL4WS in pure B2B scenarios. The paper finishes off by presenting the resulting application structure and the resulting economical implications.     

Petri net based formal analysis for multimedia conferencing services orchestration

Development of services that span over the Internet and Telecom networks is driving significant efforts towards the integrated of services offered by Telecom operators. Service-oriented communication (SOC) is a new trend in the industry to enable communication through a service-oriented architecture (SOA) and thereby package communications as services. In this paper, we firstly introduce the design and implementation for business process execution language (BPEL) based multimedia conferencing communication services orchestration, and mainly focus on the issue of guaranteeing the correctness of such applications, we presents a Petri net-based approach to analyzing the BPEL based multimedian conferencing communication services orchestration correctness and also a set of translation rules is proposed to transform BPEL processes into Petri nets. Especially, we define the correctness of multimedia conferencing services orchestration and address the verification method based on Petri nets. The algorithms and corresponding reliable issues have been proposed, such as the coverability tree for detecting flow safeness, the incidence matrix & state equation for finding reachable issues, and a transitive matrix for detecting a deadlock problem. With the Petri Net Markup Language (PNML) are introduced to transform a orchestrated services into a Petri net model, and providing an automated support for the formal analysis of their behavior. Finally, we give the conclusions.     

AO4BPEL: An Aspect-oriented Extension to BPEL

Process-oriented composition languages such as BPEL allow Web Services to be composed into more sophisticated services using a workflow process. However, such languages exhibit some limitations with respect to modularity and flexibility. They do not provide means for a well-modularized specification of crosscutting concerns such as logging, persistence, auditing, and security. They also do not support the dynamic adaptation of composition at runtime. In this paper, we advocate an aspect-oriented approach to Web Service composition and present the design and implementation of AO4BPEL, an aspect-oriented extension to BPEL. We illustrate through examples how AO4BPEL makes the composition specification more modular and the composition itself more flexible and adaptable.     

一种策略驱动的BPEL流程异常处理描述方法

针对如何提高BPEL流程的异常处理描述能力的问题,提出了一种策略驱动的BPEL流程异常处理描述方法。首先设计了一种新型的BPEL流程异常处理策略描述语言BPEH/PDL,并基于着色Petri网提出了BPEH/PDL异常处理策略的形式化描述方法。最后结合制造执行系统领域的汽车装配流水线管理系统,讨论了基于BPEH/PDL的BPEL流程异常处理策略的应用过程,以供参考。     

基于WS-BPEL的业务流程设计研究

业务流程执行语言（WS-BPEL）是当前企业业务流程管理的主流技术。在异构系统集成中,Web服务则与其他技术相结合,正发挥着越来越重要的作用。文章对Web服务合成与BPEL的关系进行了分析,研究了BPEL关键构成要素及应用BPEL进行业务流程管理的作用机制。通过一个应用实例,详细讲述了如何使用WS-BPEL进行业务流程设计。     

基于WS-BPEL 的Web 服务组合技术

随着Web服务技术的不断发展,越来越多的Web服务已经发布在互联网上。然而独立的Web服务功能通常有限,不能满足用户或企业实际应用的需求。因此,Web服务的组合显得越来越重要。介绍了Web服务组合和WS-BPEL的相关知识,使用最新的业务流程执行语言WS-BPEL描述业务流程,在J2EE集成开发环境下设计并实现了基于业务流程思想的贷款审批应用实例,在Web服务执行引擎Active BPEL上进行部署,对Web服务进行了有效的组合。     

A formal semantics for an active functional DBPL

We describe how the functional database programming language PFL is extended with an active component without compromising either its declarative semantics or its syntax. We give a formal specification of the active component using PFL itself, including event specification and detection, parameter-binding, reaction scheduling and abort handling. We describe how a user-specified function can be cast as a primitive event, and discuss the expressiveness of events and the optimisation of event detection.