{Abduction for Specifying and Verifying Web Service Choreographies}