Formalization and analysis of timed BPEL

In this paper, we are interested in formalization, analysis and checking of the BPEL language at the semantic level. We propose translating rules from BPEL language to a low-level real-time model (DATA). This model is based on true-concurrency semantics and supports at the same time timing constraints and actions durations. This transformation approach gives a formal semantics to the BPEL language and allows the formalization and the analysis of both qualitative and quantitative requirements. The resulting DATA structures are then analyzed by model checking value-based temporal logic properties (TCTL) using UPPAAL.