Abstract: Business Process Execution Language （BPEL） is a flow-based language for specifying business process behavior in Web service applications. In order to verify whether a given BPEL-based application conforms to some characteristics, this paper proposed the B

Key words: Web service composition,BPEL,Finite automaton,Formal verification