Tool Support for Safety Analysis of Service Composition and Deployment Models

This paper reports on an implementation for tool support of model-checking collaborating service compositions with deployment configurations under resource constraints.The implementation accepts UML Deployment Diagrams with an applied service deployment profile and one or more WS-BPEL orchestrations that are assigned to Web Servlets and servers in this deployment. Using model-checking techniques the tool can determine whether the configuration of deadlock-free service orchestration processes introduce deadlock scenarios when combined with resource constraints of a deployment environment. The implementation is built upon a tool suite, called WS-Engineer, which is aimed at assisting service engineers in constructing and testing various aspects of a service engineering approach, including orchestration, choreography and deployment artifacts. The tool integrates as a plug-in for Eclipse, alongside the IBM Rational software architect tool suite and others. A case study based upon a complex service grid solution, for analyzing chemical markup patterns, is used to demonstrate the accessible and practical nature of the solution.