Verifiable Model Construction for Business Processes

2021 ◽  
Vol 31 (07) ◽  
pp. 1017-1042
Author(s):  
Shunhui Ji ◽  
Liming Hu ◽  
Yihan Cao ◽  
Pengcheng Zhang ◽  
Jerry Gao
Keyword(s):  
Business Process ◽  
Business Processes ◽  
Control Flow ◽  
Service Description ◽  
Data Types ◽  
Input Language ◽  
Business Process Execution Language ◽  
Composite Service ◽  
Business Process Execution

Business process specified in Business Process Execution Language (BPEL), which integrates existing services to develop composite service for offering more complicated function, is error-prone. Verification and testing are necessary to ensure the correctness of business processes. SPIN, for which the input language is PROcess MEta-LAnguage (Promela), is one of the most popular tools for detecting software defects and can be used both in verification and testing. In this paper, an automatic approach is proposed to construct the verifiable model for BPEL-based business process with Promela language. Business process is translated to an intermediate two-level representation, in which eXtended Control Flow Graph (XCFG) describes the behavior of BPEL process in the first level and Web Service Description Models (WSDM) depict the interface information of composite service and partner services in the second level. With XCFG of BPEL process, XCFGs for partner services are generated to describe their behavior. Promela model is constructed by defining data types based on WSDM and defining channels, variables and processes based on XCFGs. The constructed Promela model is closed, containing not only the BPEL process but also its execution environment. Case study shows that the proposed approach is effective.

Making the Business Process Execution Language (BPEL) Flexible

2010 ◽  
pp. 1-20
Author(s):  
Daniela Wolff ◽  
Nishant Singh
Keyword(s):  
Business Process ◽  
Process Modeling ◽  
Business Processes ◽  
Semantic Technologies ◽  
Business Process Execution Language ◽  
Limited Degree ◽  
Process Execution ◽  
Business Process Execution ◽  
Knowledge Intensive ◽  
Execution Order

The Business Process Execution Language (BPEL) is a process modeling language which uses standard control constructs to define a workflow. But, today‘s enterprises need to be agile to cope with increasing change, uncertainty and unpredictability. Therefore, automating agile business processes is still a challenge as they are normally knowledge intensive and can be planned to a limited degree. The execution order depends heavily on the case, which has to be performed. So instead of modeling all possible cases and situations which might occur in a knowledge intensive process we introduced an approach which uses semantic technologies and rules. Business rules can be utilized to allow for case-specific adaptation of process steps. A component was developed which allow during run-time rules to automatically detect the state of the case and to determine the necessary process adaptations.

A user-aware approach for describing and publishing context aware composite Web service

2016 ◽  
Vol 12 (2) ◽  
pp. 174-193 ◽  
Author(s):  
Sihem Cherif ◽  
Raoudha Ben Ben Djemaa ◽  
Ikram Amous
Keyword(s):  
Web Service ◽  
Business Process ◽  
Design Methodology ◽  
Dynamic Adaptation ◽  
Context Aware ◽  
Business Process Execution Language ◽  
Composite Service ◽  
Content Type ◽  
Composite Web Service ◽  
Business Process Execution

Purpose The purpose of this paper is to describe the composite service and the context properties related to the users in the business process execution language (BPEL) file. Design/methodology/approach The authors’ approach allows expressing requirements by taking into account potential users’ context in addition to the functional one. Findings In this paper, the authors introduce a new context-aware approach that provides a dynamic adaptation of service compositions. Originality/value This paper introduces a user-aware approach for describing and publishing context-aware composite Web service.

Business Process Standards – Current Landscape (Landkarte aktueller Standards zur Beschreibung von Geschäftsprozessen: WS-BPEL, BPEL4People, BPEL-SPE, BPELJ, SCA)

2008 ◽  
Vol 50 (2) ◽  
Author(s):  
Matthias Kloppmann ◽  
Dieter König ◽  
Gerhard Pfau
Keyword(s):  
Life Cycle ◽  
Business Process ◽  
Business Processes ◽  
Business Process Execution Language ◽  
Service Component ◽  
Human Interactions ◽  
Service Component Architecture ◽  
Component Architecture ◽  
Business Process Execution ◽  
The Web

SummaryThe landscape of current specifications for the description of business processes consists of the Web Services Business Process Execution Language (WS-BPEL) as an adopted standard, and a number of functional extensions allowing for human interactions (BPEL4People), sub-processes with life-cycle coupling (BPEL-SPE), and Java integration (BPELJ). Also relevant for the assembly of portable, executable applications is the Service Component Architecture (SCA) which provides a model for service-based components complementing WS-BPEL. This paper provides an overview of the current business process standards landscape and its further evolution.

A New Business Process Verification Approach for E-Commerce Using Petri Nets

2020 ◽  
Vol 16 (1) ◽  
pp. 92-107
Author(s):  
Mei Zhang ◽  
Fei Feng ◽  
Zhilong Zhang ◽  
Jinghua Wen
Keyword(s):  
Petri Nets ◽  
Business Process ◽  
Business Processes ◽  
Formal Method ◽  
Business Process Execution Language ◽  
Process Verification ◽  
Process Characteristics ◽  
New Business ◽  
Business Process Execution ◽  
Logic System

The design, modeling, optimization, reengineering, and coupling of business processes in e-commerce environment have gradually become a hot research topic. Business processes must be strictly described and validated by formal methods to ensure their reliability and efficiency. This paper systematically studies the introduction of new business process characteristics into behavioral temporal logic and extend TLA to obtain a new logic system PTLA, which enriches the theoretical system of formal method of business process under the environment of e-commerce. The paper also discusses Petri nets and show how to convert Petri nets into TLA. A parallel Petri net model was built to represent the dynamic, concurrency and flexibility, and cross-organizational e-commerce business process. Finally, the use of simulation to extend the business process execution language BPEL to TLA.

Study on Custom Service Combination Based on BPEL

2012 ◽  
Vol 605-607 ◽  
pp. 2451-2456
Author(s):  
Yang Jun Cai ◽  
Zhao Le
Keyword(s):  
Web Service ◽  
Business Process ◽  
Directed Acyclic Graph ◽  
Processing Time ◽  
Business Logic ◽  
Service Description ◽  
Description Language ◽  
Business Process Execution Language ◽  
Acyclic Graph ◽  
Business Process Execution

A custom service combination based on Business Process Execution Language was put forward. It mainly studied one-off recipient and keeping the business logic order unchanged. It was proposed a solution that made the serial workflow realize the local parallelism from three aspects such as message dependency, a directed acyclic graph to workflow, and the implicit message dependency. The algorithm of implementation was also discussed. A custom service combination application of ‘stocking house transactions’ and ‘stocking house mortgage’ showed the feasibility and validity of this algorithm. The system generates the BPEL by analyzing various business stakeholders’ Web Service Description Language interface thereby determining the dependence of each business order, together with maintaining the existing business logic. The BPEL enhances the local parallel processing, and makes the overall processing time reduced.

Automated Quantitative Verification for Service-Based System Design: A Visualization Transform Tool Perspective

2018 ◽  
Vol 28 (10) ◽  
pp. 1369-1397 ◽  
Author(s):  
Honghao Gao ◽  
Huaikou Miao ◽  
Lilan Liu ◽  
Jinyu Kai ◽  
Kun Zhao
Keyword(s):  
Business Processes ◽  
Threshold Value ◽  
Qualitative Property ◽  
Input Language ◽  
Requirement Model ◽  
Graphical Visualization ◽  
Quantitative Verification ◽  
Business Process Execution ◽  
Graphic Description

Service-based systems are a new software mode for distributed business processes integration. It is difficult for traditional testing methods to verify the functional and nonfunctional requirements of software. To address this problem, this paper proposes a visual verification platform to quantitatively compute the reliability and cost for evaluating the performance of service-based systems in the design phase. First, an extended automata model namely Probabilistic Reward Labeled Transition System (PRLTS) is proposed to formalize both the functional behaviors and nonfunctional features. Then, the formal language of probabilistic model checker PRISM is introduced to show the grammar of the target verification codes that we want to transform. Second, XML description tags of Business Process Execution Language (BPEL) is parsed to generate the functional behaviors using different kinds of transformation rules, based on which the probability matrix and reward concept are employed to denote the service’s reliability and cost, respectively. Third, the PRLTS model is turned into the input language of PRISM, where the graphic description language DOT of Graphviz is used as an intermediary to display system behaviors in a visual way. The model layout allows the designer to manually adjust the behaviors of the PRLTS model, where verification codes can be dynamically updated according to the changes in modified information. Fourth, to perform quantitative verification, the verification property in the form of the Probabilistic Computation Tree Logic (PCTL) formula can be automatically generated when the requirement model of the service-based system is inputted, during which the threshold value of qualitative property will be initially computed and returned as a recommended value. This allows the user to modify the qualitative property in an interactive way. Furthermore, experimental analysis of the real-world case study demonstrates the feasibility of the proposed method. Thus, our platform provides guidance for quantitative verification and graphical visualization for effectively generating formal models and checking the quantitative properties for service-based systems.

Combining the Strengths of BPEL and Mule ESB

2014 ◽  
Vol 24 (03) ◽  
pp. 347-390
Author(s):  
Aimrudee Jongtaveesataporn ◽  
Shingo Takada
Keyword(s):  
Business Process ◽  
Business Processes ◽  
Service Oriented Architecture ◽  
Control Flow ◽  
Configuration File ◽  
Application Framework ◽  
Loosely Coupled ◽  
Technology Services ◽  
Service Oriented ◽  
Business Process Execution

Service Oriented Architecture (SOA) provides an application framework which integrates variety of technology services in a loosely coupled way. Mule Enterprise Service Bus (ESB) is a widely-used ESB product that provides important functions such as message routing, message transformation, protocol-mediation, and event handling. These functions enable Mule ESB to integrate services implemented on various platforms and technologies. However, Mule ESB does not support business logic at all. Another approach to integrate services is to use a business process language such as BPEL (Business Process Execution Language). BPEL is used to define activities along with control flow. It is limited to Web service connections. One major difference is that BPEL is capable of orchestrating a business process with programming constructs, whereas Mule ESB is capable of processing messages in many protocal connections. Both BPEL and Mule ESB have different advantages. Unfortunately, neither one is powerful enough to solve some classes of business problems. In this paper we present the COMBO framework, which merges the strengths of Mule ESB and BPEL. We develop a tool to translate an extended BPEL file to a Mule ESB configuration file. The configuration file is used within a Mule ESB to execute the process that has been described within the BPEL document. We add extension modules to the standard Mule ESB for supporting BPEL functions that Mule ESB does not provide. The extended ESB has capabilities for supporting variable assignment and conditional branches in complex business processes. Our translation can cover frequently used activities in business processes. We also present case studies that use many business activities to show how the COMBO framework supports various activity translation.

Sign in / Sign up

Export Citation Format

Share Document