A model checking approach to verify BPEL4WS workflows