Correctness of automatically generated choreography specifications

The service choreography approach has been proposed for the declarative specification of multi-party conversations between participant services, in service-oriented applications and web transactions. Constraint solvers such as Alloy Analyzer can be used for the automated generation and verification of declarative choreography specifications. This presumes a mapping between the declarative specification of business rules in Semantics of Business Vocabulary and Rules (SBVR), an OMG standard for specifying business models in structured English, and the Alloy Analyzer which is a SAT based constraint solver. This paper is concerned with the correctness of such mapping between the generated instance (choreography) in Alloy and the global graph obtained as a direct visual representation of the SBVR model specification.