Statically Detect Data Races for WS-BPEL Web Services by Constraint Solver

摘要

Nowadays, Web services are widely used because of their interoperability and reusability. Multiple Web services can be composed following some business logic specified by BPEL (Business Process Execution Language) scripts. Since BPEL scripts allow specifying concurrent workflow, typical concurrency problems, such as data race, atomicity violation and order violation, also commonly occur in BPEL scripts. These issues are hard to detect and reproduce due to their non-determinism and the special language features of BPEL. In this paper, we implement a tool to detect data races for WS-BPEL based on static analysis approach and constraints solver. Our system is based on three key concepts: (1) a preprocess model to record necessary information, (2) a thorough Happens-Before model of WS-BPEL concurrency, (3) constraint encoding to transfer Happens-Before relationship to constraints and check if there is a feasible solution (namely data races) by Z3-Str solver. We evaluate the usability and performance of our tool on 10 benchmark programs with effective results.