Formal Modeling and Analysis of Business Process Timed Constraints

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