A Model Checking Approach to Verify BPEL4WS Workflows