Abduction for Specifying and Verifying Web Service Choreographies.