Different standards and languages are proposed in the literature to model the composition of Web services. Unfortunately these languages are essentially syntactic and thus contain much ambiguity and inconsistency. In addition, the formal verification of the proposed languages is impossible. In this paper, the authors propose a transformation approach allowing the formal representation, analysis and refinement of Web services compositions. Both timed constraints and the durations of interactions between these services are taken into account. The authors present a mapping from Web services described in the BPEL language to an abstract specification written in the real-time language D-LOTOS which is based on true-concurrency semantics.
Formal verification of user-level real-time property patterns