The Service-Oriented Architecture (SOA) approach to building systems of application and middleware components promotes the use of reusable services with a core focus of service interactions, obligations and context. Although services technically relieve the difficulties of specific technology dependency, the difficulties in building reusable components is still prominent and a challenge to service engineers. Engineering the behaviour of these services means ensuring that the interactions and obligations are correct and consistent with policies set out to guide partners in building the correct sequences of interactions to support the functions of one or more services. Hence, checking the suitability of service behaviour is complex, particularly when dealing with a composition of services and concurrent interactions. How can we rigorously check implementations of service compositions? what are the semantics of service compositions? how does deployment configuration affect service composition behaviour safety? To facilitate service engineers designing and implementing suitable and safe service compositions we present in this paper an approach to consider different viewpoints of service composition behaviour analysis. The contribution of the paper is threefold. Firstly, we model service orchestration, choreography behaviour and service orchestration deployment through formal semantics applied to service behaviour and configuration descriptions. Secondly, we define types of analysis and properties of interest for checking service models of orchestrations, choreography and deployment. Thirdly, we describe mechanical support by providing a comprehensive integrated workbench for the verification and validation of service compositions.

Links

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

Tools

1. LTSA WS-Engineer