Abstract
Guaranteeing the correct coordination of distributed applications that are built up as networks of autonomous participants, e.g., software components, web services, online resources, software as a service (SaaS) peers, is inherently challenging. This is obvious when the current distributed applications involve a collaboration between loosely-coupled services on distinct providers; the ordering of interactions that may further affects the dependencies between different participants, including control flow dependencies (e.g., a given service invocation must occur before another one), time constraints, and transactional dependencies. This complexity of the development of distributed applications illustrates how important the techniques and approaches for designing and coordinating the service interactions between distinct participant services to ensure that the overall goal of the collaboration between participant services is achieved. Standardisation efforts to date have resulted in the Web Services Choreography Description Language (WS-CDL), a specification protocol advocated by W3C. WS-CDL and other modeling languages (e.g., UML2) provide various divergent semantics and less user-friendly graphical notation. On the other hand the formal approach would allow unambiguous specification and verification of the intended collaboraton. In this research work, a declarative approach was proposed for specifying coordination of distributed applications involving distinct participant services which is being able to verify that it is correct. The proposed approach could captures and describing the complex interactions that involves the ordering of service interaction based on the given global constraints. A new model using a declarative approach, an OMG standard Semantics of Business Vocabulary and Rules (SBVR) model was introduced for specifying service choreography. This SBVR model is then formulated and transformed into Alloy model using Alloy Analyzer for verification. A fully automated SBVR2Alloy tool was implemented for transforming from the developed SBVR model into the Alloy model. This proposed model is targeted to enable the practitioners (business analysts, developers) to devise and set up the service choreographies that realise their collaborations by generating the automated verifiable choreography model.