Specification and Verification of a Composition of Services

In this chapter, we show how our model can be used to specify and verify a sequential flow of data-centric Web services. A sequential flow of services is essentially made up of a number of individual services that are executed in a specific order and are integrated by means of sequential composition, loops and conditional statements. This is a traditional service composition problem where a service consumer integrates the functionalities of two or more services in order to construct a new service that provides a more complex functionality. The challenge that we are addressing here is how to guarantee that the integration will have the intended final effect on the underlying data.