Interface theory-based formalisation, verification of orchestrationin BPEL4WS