Formal Methods for Service Composition