Abstract
Service choreography describes the interaction across different participating services capturing the ordering constraints of global message exchanges. Semantics of Business Vocabulary and Rules (SBVR) model, an Object-Oriented Management (OMG) standard is proposed to specify services interaction (service choreographies), The specification focuses on a deontic rule expressing both prohibition and obligation which can be progressively helpful in working with coordinating service interactions. Then Alloy Analyzer, a relational constraint solver, is used to transform a developed service choreographies, an SBVR model into an Alloy model. This transformation allows to generate and to verify, the choreography for the developed SBVR model and the realisability of the generated choreography, automnatically.