目前,随着Web服务技术的不断推广与应用,面向服务的计算已经成为软件工程领域的研究热点。通过重用现有服务,将服务进行组合,企业能够更为快速有效的构建具有灵活、松耦合特点的分布式系统。如何利用现有的服务资源,搭建结构更复杂,功能更强大的业务系统,以及验证服务组合与业务需求的一致性,是当前研究的一个重点。针对目前缺乏一种支持图形化表示、形式化验证的服务组合模型,本文提出了基于接口自动机的服务组合模型,该模型扩展了接口自动机,能够同时描述服务流程与服务语义。本文设计了BPEL流程到接口自动机模型的转换算法。模型利用接口自动机并发组合算法实现服务流程的组合,通过检测接口自动机的行为模型来验证服务流程与业务需求的一致性。实验表明,基于接口自动机的服务组合模型能够准确、完备的表达BPEL流程,同时模型能够准确的验证服务流程与业务流程是否一致。针对目前缺乏一种对服务质量(QoS)需求的验证方法,本文在接口自动机模型的基础上,提出了一种对服务QoS需求进行验证的方法。该方法在将服务质量属性进行定量描述的基础上,设计了一种针对QoS需求的形式化表述策略。针对BPEL对QoS属性支持不足的缺点,在BPEL上扩展了描述QoS属性的标签。本方法能对由接口自动机模型组合后的组合服务中每一项业务功能均进行QoS需求验证,通过和其他QOS验证方法实验比较,本方法能够更高效的验证QoS需求。本文主要关注于服务组合验证方面的研究,包括接口自动机的服务组合模型、组合服务与业务功能一致性的验证以及QoS需求验证。对以上问题提出了有效的解决方案,对于推进Web服务组合与验证技术的理论研究提供了新思路和方法。