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

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

Manuel Mazzara, Michele Ciavotta
DOI: 10.4018/ijssoe.2014100103
(Individual Articles)
No Current Special Offers


Web Services provide interoperable mechanisms for describing, locating and invoking services over the Internet; composition further enables to build complex services out of simpler ones for complex B2B applications. While current studies on these topics are mostly focused - from the technical viewpoint - on standards and protocols, this article investigates the adoption of formal methods, especially for composition. The authors logically classify and analyze three different (but interconnected) kinds of important issues towards this goal, namely foundations, verification and extensions. The aim of this work is to individuate the proper questions on the adoption of formal methods for dependable composition of Web Services, not necessarily to find the optimal answers. Nevertheless, the authors still try to propose some tentative answers based on our proposal for a composition calculus, which they hope can animate a proper discussion.
Article Preview


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 (, XML (, 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

Enabling users to describe business process activities as Web services and define how they can be connected to accomplish specific tasks.

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.



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.

Complete Article List

Search this Journal:
Volume 13: 1 Issue (2023): Forthcoming, Available for Pre-Order
Volume 12: 2 Issues (2022): 1 Released, 1 Forthcoming
Volume 11: 2 Issues (2021)
Volume 10: 2 Issues (2020)
Volume 9: 2 Issues (2019)
Volume 8: 4 Issues (2018)
Volume 7: 4 Issues (2017)
Volume 6: 4 Issues (2016)
Volume 5: 4 Issues (2015)
Volume 4: 4 Issues (2014)
Volume 3: 4 Issues (2012)
Volume 2: 4 Issues (2011)
Volume 1: 4 Issues (2010)
View Complete Journal Contents Listing