Formalizing Timed BPEL by D-LOTOS
Imed Eddine Chama, Nabil Belala, Djamel Eddine Saïdouni · International Journal of Embedded and Real-Time Communication Systems · 2014
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.