In this chapter we discuss a model-based approach to the analysis of service interactions for web service choreography and their coordinated compositions. The move towards implementing web service choreography requires both design time verification and execution time validation of these service interactions to ensure that service implementations fulfil requirements for multiple interested partners before such compositions and choreographies are deployed. The approach employs several formal analysis techniques and perspectives, and applies these to the domain of web service choreographies and the compositional implementations that each role in these choreographies must satisfy. Our approach models the service interaction designs of choreographies (in the form of UML style Message Sequence Charts), the service choreography descriptions (in the form of WS-CDL – the Web Service Choreography Description Language) and the service composition processes (in the form of BPEL4WS - the Business Process Language for Web Services). Analysis techniqueson these models show whether service interactions are “compatible” for service choreography. We translate between UML and Web Service specifications into the Finite State Process (FSP) process algebra notation. Where interactions deviate from choreography rules, the interaction sequences can be shown back to user of the approach in an easy and accessible way, in the UML form. An example of using this approach follows the scenario set at the beginning of this monograph where a client requires a series of services to be called for reservations, trip planning and navigational updates. The example is used to illustrate undertaking the approachfrom design, implementation and maintenance perspectives and reviewing interaction sequences of a series of co-operating services. The described approach is supported by a suite of cooperating tools (collectively known as the Labelled Transition System Analyser – LTSA) for specification, formal modelling, simulation, animation and providing verification results from choreographed web service interactions.

Links

Further details will be added for related links and this publication.

Tools

Further details will be added for related tools and this publication.