Agent Societies and Service Choreographies: a Declarative Approach to Specification and Verification