This book consists of eight tutorial papers on the use of formal methods for Web services. The very technical papers are written for “young computer science researchers,” with the following stated purpose:
to [establish] the missing theoretical foundations of state-of-the-art technologies, so [as] to fix rigorous semantic and logic frameworks for the analysis and verification of [service-oriented computing] SOC and [Web services] WS systems ... [and to understand] the key distinguishing features of SOC ... in technology agnostic terms.
This purpose is certainly laudable, and the stated emphasis on semantics and understanding is very welcoming. Many of the papers mention the existing issues with semantics, such as “the lack of unambiguous semantics of [business process execution language] BPEL,” and note “the lack of semantic information in the description of services.” While some of the papers state that these two problems need to be satisfactorily solved, they do not emphasize semantics. Furthermore, van der Aalst et al.’s paper properly (although anthropomorphically) states: “In order to find compatible pairs of services, services need to know each other. ... One common approach is where a service shows its own specification or implementation.” (That being said, showing the implementation is probably an incorrect approach.) On the other hand, Bruni’s paper explicitly states: “We disregard those aspects related to the so-called semantic Web, like ontologies for classifying services.” Under these circumstances, it is unclear how one finds in the repository a service that provides whatever the caller needs.
It may be instructive to consider the authors’ approaches to formal methods within the framework of Parnas’ rather skeptical paper [1]. In particular, some aspects of these papers look like instantiations of patterns presented by Parnas. For example, Bruni’s statement that “a new calculus ... is the main objective of this tutorial” is, at least to some extent, an instantiation of Parnas’ observation that “many research papers are written as if the mathematics were all that matters.”
Readers who are looking for information on the semantics of contracts--for example, for service discovery--will find the following, in Bravetti and Zavattaro’s paper: “The service contract describes the sequence of input/output operations that the service intends to execute within a session of interaction with other services.” Moreover, Padovani’s paper states: “The presented theory of contracts is based on (a variant of) the CCS language whose terms describe interactions without any information on the content of the exchanged messages.”
This approach is operational rather than declarative, which leads to possible problems that have been noted in other works [1,2]. Furthermore, how can a Web service be discovered in a repository--as Bravetti and Zavattaro state, by “independently sending queries to registries”--or even be used if the semantics of what it is and what it does is not clear? These papers lack significant contributions to these questions.
More than one paper uses meaningful names in place of operation definitions. Relying on meaningful names in specifications is a well-known fallacy in the business-modeling world, since the contexts used for understanding the names’ meanings vary by stakeholder. While van der Aalst et al. explicitly mention that the incompatibilities of names and semantics with similar message types present a problem when integrating independently developed services, these same authors define behavioral incompatibility as an “order in which messages are expected or transmitted.”
Several papers provide clear motivations: Carbone et al. explain the need for interactional exceptions and nonbinary (multiparty) asynchronous session types; Padovani explains the need for a synchronous orchestrator; Bravetti and Zavattaro explain the distinction between choreography and orchestration; and van der Aalst et al. clearly present motivations for service interaction patterns, emphasize concepts, and use realistic toy examples. Two other outstanding papers by van der Aalst [2,3] are perfect prerequisites for less-initiated readers, as they will provide an appropriate context for this book.
Service composition, and especially the semantics of the composite service based on the semantic properties of its component services, is a very important and interesting problem. Unfortunately, in this collection, the semantic aspects of “what the service does” are at best presented operationally, or otherwise hidden in technicalities. Even in the toy-ish examples, the specifications are very technical, detailed, and not too interesting; thus, one of the most important objectives of a formal specification--to serve as a basis for unambiguous understanding by all stakeholders, after being translated into a rigorous, stylized natural language [4]--is not achieved. The soft aspects of model quality, like readability and understandability, are not addressed. Even the realistic example of an e-payment service case study is not very interesting: its specifications are quite obvious and look like rather sophisticated flowcharts with meaningful names. Unfortunately, many authors’ references to semantics may be exemplified by the following statement: “However, if the specifications of these messages and of the data types contain semantic information ...” The use of a specification that does not contain such information is very limited--at least for a business user--and this otherwise useful and interesting book would benefit from a greater emphasis on such information. One last note: the book lacks a subject index.
