Using formal methods to develop WS-BPEL applications

In recent years, WS-BPEL has become a de facto standard language for the orchestration of Web services. However, there are still some well-known difficulties that make programming in WS-BPEL a tricky task. In this paper, we first point out major loose points of the WS-BPEL specification by means of many examples, some of which are also exploited to test and compare the behaviour of three of the best-known freely available WS-BPEL engines. We show that, in fact, these engines implement different semantics, which undermines the portability of WS-BPEL programs over different platforms. Then we introduce View the MathML sourceBlite, a prototypical orchestration language equipped with a formal operational semantics, which is closely inspired by, but simpler than, WS-BPEL. Indeed, View the MathML sourceBlite is designed around some of WS-BPEL’s distinctive features such as partner links, process termination, message correlation, long-running business transactions, and compensation handlers. Finally, we present View the MathML sourceBliteC, a software tool supporting a rapid and easy development of WS-BPEL applications via the translation of service orchestrations written in View the MathML sourceBlite into executable WS-BPEL programs. We illustrate our approach by means of a running example borrowed from the official specification of WS-BPEL.