Specifying and Verifying Contract-driven Composite Web Services: a Model Checking Approach