Database of Research Tools Developed Using CADP

Formal Modeling and Validation of BPEL-based Web Service Composition

Organisation: North China University of Technology, Beijing (CHINA)

Functionality: Verification of BPEL Web services.

Tools used: CADP (Construction and Analysis of Distributed Processes)

Period: 2012

Description: WS-BPEL (Web Service-Business Process Execution Language, BPEL for short) makes possible the construction of elaborate business processes by composing several simple Web services (WS). Since the WS are dynamic and the WS-Policy is changing, there may be problems in the business process of BPEL described composition. If an inaccurate business process is deployed without verification, problems will arise when running it. Repairing the system will be costly, too. Therefore, it is necessary to verify the business process before coming into use.

This work proposes a new formal model for WS-BPEL described WS composition by using the specification language LOTOS. This enables to carry out model checking using the CADP toolbox to ensure the validity of the model. A BPEL description is translated into a three-level LOTOS model consisting of a client process, an orchestration process, and several independent WS processes. BPEL basic and structured activities are translated into LOTOS processes in a compositional manner. An automatic translator from BPEL to LOTOS was built, which enables the designer to specify temporal properties in mu-calculus and to verify them on the LOTOS model by using the EVALUATOR model checker of CADP. The approach is illustrated by an example of BPEL business process describing a bank loan service.

Conclusions: This work confirms that value-passing process algebras are appropriate for modeling WS compositions described in BPEL. The automatic connection from BPEL to these formal languages provides to business process designers all the analysis functionalities available from the concurrency domain.

Publications: [Zhao-Wang-Sun-Wei-12] Huiqun Zhao, Wenwen Wang, Jing Sun, and Ying Wei. "Research on Formal Modeling and Verification of BPEL-based Web Service Composition". Proceedings of the 11th IEEE/ACIS International Conference on Computer and Information Science ICIS'2012 (Shanghai, China), IEEE Computer Society Press, pages 631-636, June 2012.
Available on-line at:

[Zhao-Sun-Liu-12] Huiqun Zhao, Jing Sun, and Xiaodong Liu. "A Model Checking Based Approach to Automatic Test Suite Generation for Testing Web Services and BPEL". Proceedings of the Asia-Pacific Services Computing Conference APSCC'2012 (Guilin, China), pages 61-69. IEEE Computer Society Press, December 2012.
Available on-line at:

Huiqun Zhao
Department of Computer Science
North China University of Technology

Further remarks: This tool, amongst others, is described on the CADP Web site:

Last modified: Thu Feb 11 12:23:11 2021.

Back to the CADP research tools page