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

PREFACE

The last decade has seen a major shift toward a service-oriented paradigm. Companies have been promoting their software as services to be used by other applications over the web, and the ubiquity of the Internet has allowed these services to be used from across the globe. The major results of this shift include resolving software interoperability issues, increased reusability of code, easy interapplication communications, and significant cost reduction, which have created significant business opportunities for companies offering webservices.

However, individual webservices seldom meet all the business requirements of an application. Usually, an application interacts with several web services, as required by its workflow. Considering that this might require a number of activities, including sharing data with multiple services, tracking the response for each service request, and detecting and compensating service failures, a domain-specific language is generally used for service composition. Each service's offerings are outlined by interfaces that also serve as a basis for service composition.

Nevertheless, any error or omission in these published interfaces could result in a number of glitches in the composition and the overlying application. This is exacerbated further by dynamic service composition techniques wherein services could be added, removed, or updated at runtime. Consequently, service-consuming applications depend heavily on verification techniques for reliability ...