Verification of Communication Protocols in Web Services: Model-Checking Service Compositions

CHAPTER 4

WEB SERVICES

In recent years, companies have been actively exposing their software as a service to be used by other applications over the network. These services have uncovered various business opportunities by exploiting the ubiquitous nature of the web. They adhere to the associated service description, irrespective of the underlying implementation. However, as shown in Figure 4.1, these services, by themselves, might not be very useful. In the scenario illustrated, a customer needs to make several individual web-service calls to complete a shopping event. Furthermore, the calls need to be made in a specific order wherein the reference from the preceding call is used in the succeeding invocation. Apart from being a cumbersome and error-prone process, this scenario unnecessarily exposes the underlying business logic of the application.

Figure 4.2 illustrates an alternative scenario wherein the business logic is encapsulated within the application. The customer only needs to provide the payment and address details to finish shopping. However, this necessitates composing the involved web services based on the business logic of the application. Such a state of affairs has resulted in the emergence of different service composition languages. In recent years, the Business Process Execution Language (BPEL) has emerged as the de facto standard language for composing web services.

FIGURE 4.1 Using individual exposed services for online shopping.

FIGURE 4.2 Using service ...