随着Web服务的出现和推广,Web服务组合技术已经成为近年来的研究热点。Web服务的业务流程执行语言(BPEL4WS)作为一种基于业务流程的服务组合方法,建模理论基础比较薄弱,组合的正确性难以保证。因此业务流程的正确性、无死锁性、行为一致性等问题,在它正式被实施前必须得到验证。针对现有的BPEL4WS验证方法使用的形式化方法较为复杂、不能以全面简洁的方法直观的表达需求规约、无法很好的满足实际的应用需求等不足之处,本文在基于UML顺序图作为需求规约的基础上,提出了一种利用接口自动机对BPEL4WS的行为一致性进行验证以及适配的方法。本文的主要工作包含以下几个方面:1.文章首先着重对BPEL4WS的行为一致性问题进行了分析,然后简单的介绍了Web服务组合语言BPEL4WS和Web服务描述语言WSDL,阐述了BPEL4WS与WSDL两者之间的关系,介绍了接口自动机的基本语法以及接口自动机在描述组件接口和组件组合方面的突出特点,最后分别给出了BPEL4WS与WSDL到接口自动机的转换规则。2.针对BPEL4WS的行为一致性分析与验证问题,使用UML顺序图表示BPEL4WS的需求规约并将其投影为接口自动机的一个执行片段,使用接口自动机及接口自动机网络来描述BPEL4WS的行为设计模型,在此基础上对BPEL4WS的应用实现与需求规约是否满足行为一致性进行了分析与验证并给出了相应的验证方法。3.在对BPEL4WS行为不一致的原因进行分析的基础上,文章提出了一个基于接口自动机的适配器构造算法,针对由于Web服务接口不匹配而导致的BPEL4WS应用实现与需求规约的行为不一致进行了接口适配。全文以出差安排业务过程为例,将其BPEL4WS与WSDL转换后的接口自动机组合为接口自动机网络,使用UML顺序图表示其需求规约,说明了基于接口自动机的BPEL4WS的行为一致性验证和适配的方法的有效性.