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 Blite, a prototypical orchestration language equipped with a formal operational semantics, which is closely inspired by, but simpler than, WS-BPEL. Indeed, Blite 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 BliteC, a software tool supporting a rapid and easy development of WS-BPEL applications via the translation of service orchestrations written in Blite into executable WS-BPEL programs. We illustrate our approach by means of a running example borrowed from the official specification of WS-BPEL.

► We point out major loose points of the Web service orchestration language WS-BPEL.
► We show that some freely available WS-BPEL engines implement different semantics.
► We introduce the prototypical orchestration language Blite.
► Blite is inspired by WS-BPEL but is equipped with a formal operational semantics.
► We present BliteC, a tool supporting an easy development of WS-BPEL applications.