Transforming BPEL into Annotated Deterministic Finite State Automata for Service Discovery