|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| 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: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6211163 [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: http://ieeexplore.ieee.org/stamp/stamp.jsp?tp=&arnumber=6478199 |
| Contact: | Huiqun Zhao Department of Computer Science North China University of Technology China Email: zhaohq@ncut.edu.cn |
| Further remarks: | This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software |
Back to the CADP research tools page