{Model-based Verification of Web Service Composition}