介绍了接口自动机的基本语法，针对目前最主要的一种描述和执行基于工作流模式的Web服务组合的规范——Web服务商业流程执行语言 (business process execution language for Web services，BPEL4WS)，定义了接口自动机和BPEL4WS之间的概念映射，并给出了BPEL4WS的基于接口自动机的形式化模型，最后通过一个案例给出了BPEL4WS到接口自动机的映射及验证的方法。