Issues about the Adoption of Formal Methods for Dependable Composition of Web Services

Introduction

Service Oriented Architecture and the related paradigm are modern attempts to cope with old problems connected to B2B and information interchange. Many implementations of this paradigm are possible but presently the so called Web Services look to be the most prominent, mainly because the underlying architecture is already there; it is simply the web which has been extensively used in the last 15 years. We can easily exploit HTTP (W3C.org), XML (W3C.org), SOAP (Box et al., 2000) and WSDL (Christensen et al., 2001). The World Wide Web provides a perfect basic platform to connect different companies and customers but cannot fulfill all the needs that use to arise in this context. It is perfect for the interconnection on a point-to point basis, but one of the B2B complication is the management of causal interaction between different services and the way in which the messages between them need to be handled, not always in a sequential way for example. This area of investigation is called composition, i.e. the way to build complex services out of simpler ones (Peltz, 2003). So, the need for workflow technology is evident. The positive thing is that we had this technology investigated for decades and we have also excellent modeling tools providing verification features that are grounded in the very active field of concurrency theory research.

Different organizations are working on composition proposals. The most important in the past have been IBM’s WSFL (Leymann, 2001) and Microsoft’s XLANG (Thatte, 2001). These two have then converged in Web Services Business Process Execution Language (Jordan & Evdemon) (WS-BPEL or BPEL for short), which is presently an OASIS Standard. The language allows workflow-based composition of services and in the committee members words the aim is

Earlier versions of the language were not so clear, the specification was huge and many points not very clear, especially in relation to the recovery framework and the interactions between different mechanisms (fault handlers and compensation handlers). The sophisticated implicit mechanism of recovery was confused. However, in the final version of the specification (which is lighter and clearer) fault handling during compensation has been clarified. WS-BPEL represents a necessary business tradeoff where not all the single technical choices have been done considered the entire set of options. For this reason, critics to the specification may lead to further improvement. In the following, we present a few questions that could help us in this process. We tried to logically separate these questions in three areas: Foundational questions, Verification questions and Extensions questions. For each area you can find a dedicated section.

Foundations

The need for formal foundation has been discussed in recent last years and several attempts of using some kind of formal methods in this setting have been speculated. Some communities, for example, criticized the process algebra option (van der Aalst, 2003) promoting the Petri nets choice. Do we really need a formal foundation and which kind of formalism do we need? It is crucial to understand the notion of killer applications and to identify a possible selling point for our work. Furthermore, having worked for some time on Semantic Web Services, we are still trying to figure out whether adding a semantic description of services may bring a significant value in comparison with analysis and development costs spent over the last few years. So it is worth spending some time to investigate this issue as well. This section discusses more broadly these general and foundational issues.