随着Web服务技术的迅速发展,越来越多的的Web服务运行在Internet上,但单个的Web服务功能有限,难以满足日益增长和不断变化的用户需求。因此,如何将已有的、运行在异构平台上的Web服务组合起来,以提供给用户更为强大和增值的功能,成为Web服务研究领域中的一个热点。由于已有的Web服务可能是彼此独立地开发,以不同语言实现,运行在不同的、异构的平台上,因此Web服务组合存在的问题有:如何描述Web服务的动态行为,如何定义和描述Web服务间的交互的逻辑顺序以保证Web服务的动态行为的匹配性,如何保证Web服务之间传递消息的数据类型的一致性,如何对组合的Web服务进行验证和测试以确保执行结果的正确性。目前已经提出的Web服务组合规范如BPEL4WS、WS-CDL都是基于XML的描述性语言,缺乏一种形式化模型来表达语言的语义以及形式化验证方法来保证用这些规范所定义的Web服务组合的正确性。同时,由于参与Web服务组合的各个子服务都运行在分布式异构的环境下,因此想依靠组合的Web服务的实际运行来检测组合中的错误是代价昂贵的并且几乎是不可能的,因此对Web服务组合的形式化验证也是必须的而且是非常重要的。解决上述问题的一个行之有效的办法就是针对Web服务组合规范如BPEL4WS、WS-CDL建立合适的形式化模型,形式化地定义和描述Web服务组合的动态交互行为,利用Web服务组合的形式化模型对Web服务组合的性质如死锁避免、数据类型一致性和动态行为的匹配性进行检查和验证,以保证Web服务组合的动态行为的匹配和数据类型的一致性。因此,针对Web服务组合规范BPEL4WS和WS-CDL,研究了基于工作流的Web服务组合形式化模型以及如何利用Web服务组合的形式化模型对Web服务组合的动态行为的匹配和数据类型的一致性进行验证。针对Web服务组合规范BPEL4WS,分别建立了BPEL4WS到Pi-演算和CSP的概念映射,在此基础上,建立了基于Pi-演算和CSP的BPEL4WS形式化模型;同时给出了从BPEL4WS到Pi-演算和CSP进程的自动转换算法和模型的验证方法。针对Web服务组合规范WS-CDL,建立了基于全局的形式化模型框架AbstractWS-CDL,在此基础上利用Abstract WS-CDL对WS-CDL中各类行为进行了形式化描述;同时定义了将全局模型框架Abstract WS-CDL映射到基于Pi-演算的局部BPEL4WS模型的映射规则,并给出了全局模型框架和局部模型一致性的形式化定义;然后给出了全局和局部二个层次的模型验证方法以及全局模型框架和局部模型一致性的验证方法。利用基于Pi-演算的形式化方法研究和给出了二个Web服务的强互相容和弱互相容的形式化定义,在二个Web服务弱互相容定义的基础上,定义了二个Web服务之间互投影的算法,进而给出了多个Web服务互相容的形式化定义;然后给出了Web服务的可替换性的判断准则和二个Web服务相容性的检测算法。研究和给出了类型化的BPEL4WS形式化模型和类型化的Abstract WS-CDL形式化模型框架,特别是提出了进程类型假设集的外延和进程类型假设集相容性的概念,并且给出了进程类型假设集的合并算法;在此基础上,定义了全局会话和局部进程类型良好性的推理规则和捕获由于类型不一致而导致运行时错误的操作语义。同时,给出了从类型化的全局模型框架到类型化的局部模型的映射规则;然后,针对类型化的Abstract WS-CDL,给出了全局会话类型安全性质的证明。根据所建立的全局和局部模型,给出了一个自顶向下的Web服务组合实现框架iFrame4WS,在该框架中将Web服务组合的过程划分为描述层、抽象层和执行层,并通过抽象层的形式化模型和形式化验证来保证Web服务组合的的动态行为的匹配和数据类型的一致性。