在面向服务的计算(SOC)中,服务已成为Web应用中的最主要的元素。网络技术和因特网的广泛应用方便了客户对Web服务的访问,也使得各个公司能够以非常灵活的方式合作,将他们的服务整合起来,以提供更加复杂的、增值的产品和服务。服务的协作和组合同时带来了很多问题和挑战,突出表现为服务的可组合性、同步性、协调性、正确性验证等等。近年来,很多研究者为此展开了相关研究工作,已经产生一些研究成果。鉴于其潜在的应用价值和存在的难点问题,引起了学术界和工业界的普遍关注,成为一个研究热点。本文围绕Web服务及组合展开论文的相关工作,主要工作如下：1)对Web服务描述语言进行了广泛的分析与研究,提出了扩展静态的WSDL以描述服务动态行为的策略,并提出了从扩展的WSDL语言到TLA语言转换算法,从而用TLA对服务进行形式化描述和规范。2)基于服务的有限状态自动机(FSA)模型,对服务进行组合,通过对各个服务的TLA规范按不同组合方式进行组合和变换就得到了描述服务组合过程进行TLA规范,并对之提出了相应的组合算法。3)针对上面的组合规范,用TLC模型检验器遍历模型,检验规范是否成立,验证组合系统的安全性、正确性、灵活性等问题。4)讨论了从BPEL4WS到TLA的转变算法,并基于上述算法开发从BPEL4WS自动转变到TLA的工具。5)使用定性方法来表示各个用户的偏好；并提出了多用户不完全偏好情形下的推理算法；还提出了用户的偏好序列中存在冲突时的处理方法和相应的算法。6)扩展了F. Rossi等人提出的Rank机制,提出了Subrank机制,并给出了一个实例说明以上方法如何用于实际的服务选择中。