{Declarative Specification and Verification of Service Choreographies}