Service interactions coordination (Choreography Model) using a declarative approach from semantics of business vocabulary and rules (SBVR) models

Coordinating the interactions between autonomous participant services from different providers is a complex challenge when developing distributed applications. This research aims to develop an improved technique for modelling, generating, and verifying services interaction applying choreography approach which emphasises on a declarative approach based on the Object Management Group (OMG) standard, that is Semantics of Business Vocabulary and Rules (SBVR). An enhanced choreography model, called an SBVR model, can develop the choreography model by employing deontic rules, including both obligation and prohibition rules. The generated SBVR model is then transformed into an Alloy model using the Alloy Analyzer constraint solver, enabling automatic generation and verification (conformance and realisability) of the choreography model. This study also applies a global graph for proving the correctness of transformation SBVR model into Alloy model. In conclusion, this research has strived to add new knowledge to the current research by improvising the technique for modelling and generating the choreography model, allowing the conformance and realisability verification, through an SBVR-based choreography approach. The injection of prohibition rules into the model enables the choreography specification to capture not only what needs to be obligated but also what needs to be prohibited. The contributions of this research are significant in enabling non-expert users to effectively coordinate services and validate choreography models. This is achieved through the direct reading of the SBVR model, expressed in natural language, thereby enhancing comprehension for users without specialised expertise. The developed SBVR model, represented in formal logic, is also suitable for parsing and verification purposes.