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

CHAPTER 1

INTRODUCTION: SERVICE RELIABILITY

Service-oriented architecture (SOA)–based applications are built as an assembly of existing web services wherein the component services can span across several organizations and have any underlying implementations. These services are invoked in a sequence based on the business logic and on the workflow of the application. They have alleviated software interoperability problems and catapulted SOA into the forefront of software-development architectures. The rapid inroads made by such applications can be attributed to their agility, maintainability, and modularity.

SOA-based applications require software components to be exposed as services. Each service has an interface that outlines the functionality exposed. Ideally, an application is designed by discovering appropriate services, using their interfaces, and composing them. Such static compositions require the services involved to be perpetual and consistent throughout the lifetime of the application. Microsoft Biztalk [52] and Oracle WebLogic [38] are among popular static composition engines.

However, existing web services can break, and newer (and probably better) services can surface. Furthermore, a change in the business logic of an application during its lifetime might necessitate that additional web services be composed dynamically. Such a state of events has culminated in dynamic web service composition. Compared to their static counterparts, an application based on dynamic composition ...