Interface automata-based formal model for BPEL4WS Web service composition
基于接口自动机的BPEL4WS Web服务组合形式化模型

This paper introduced basic syntax of interface automata. For the most important kind of specification of specifying and executing workflow-based Web service composition-business process execution language for Web services(BPEL4WS), defined the conception mapping between interface automata and BPEL4WS and presented a interface automata-based formal model for BPEL4WS. Introduced the model verification method through a case study.