University of Surrey

Test tubes in the lab Research in the ATI Dance Research

Generating verifiable service choreographies from SBVR models.

A.Manaf, Nurulhuda (2018) Generating verifiable service choreographies from SBVR models. Doctoral thesis, University of Surrey.

Final_PhD_Thesis_Nurulhuda.pdf - Version of Record
Available under License Creative Commons Attribution Non-commercial Share Alike.

Download (5MB) | Preview


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.

Item Type: Thesis (Doctoral)
Divisions : Theses
Authors :
A.Manaf, Nurulhuda
Date : 28 February 2018
Funders : Ministry of Higher Education Malaysia
Contributors :
ContributionNameEmailORCID, Sotiris
Depositing User : Nurulhuda A Manaf
Date Deposited : 05 Mar 2018 09:54
Last Modified : 05 Mar 2018 09:54

Actions (login required)

View Item View Item


Downloads per month over past year

Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800