目前服务组合的研究得到了学术界和工业界的广泛关注,国内外研究者提出了众多的服务组合方法。尽管工业界已经开发了许多标准来描述Web服务,但是由于缺少全面的工程方法,开发基于Web服务的系统仍旧是一个具有挑战性的问题。目前的问题主要是非形式化的工程方法对于开发人员来说是容易理解的,但是由于在需求描述和系统建模上的二义性,在质量保证等方面具有缺陷。而形式化的方法通过形式化的描述、验证提供了保证软件系统正确性的潜力。但是由于他们的复杂性和大规模系统开发的技术难度,很少有开发人员实际中使用它们。SOFL(Structured Object-oriented Formal Language)是一种结构化、面向对象和形式化的工程方法,具有简单、可视化和精确的特点,能把传统的形式化方法和软件工程有机结合地起来。但是目前SOFL语言只提供的是一种严密、系统、有效地软件开发方法,主要用于描述系统功能性需求和设计规范,而对Web Service技术和SOA(Service-Oriented Architecture)架构联系得不够紧密。针对上述问题,本文主要研究设计时的服务组合方法,将SOFL与Web服务结合起来。具体内容包括:面向服务的SOFL描述需求的方法;SOFL的CDFD(Condition Data Flow Diagram)图与BPEL(Business Process Execution Language)流程结构的转换规则;两阶段服务发现匹配机制;基于SOFL的Web服务流程验证以及设计基于SOFL的Web服务组合系统框架和实现原型系统。本文主要工作是将SOFL的相关理论与Web服务的相关技术结合起来,并且引入本体技术,从而完成设计时的Web服务的匹配和组合。首先根据领域本体构建本体库,并根据用户提出的需求,使用SOFL对需求进行描述,并且根据本体库,对需求进行语义标注便于之后匹配服务。对于服务提供商提供的服务,使用本体库中的领域本体,对服务进行语义标注,再使用SOFL对服务中的前置后置条件进行描述,便于之后与需求进行匹配。然后,本文将SOFL中的CDFD图转化为BPEL流程结构,并根据每个SOFL中的Process对服务进行两阶段匹配查找,将查找到的一个或者一组服务装入BPEL流程结构中,并且对组合出的流程进行形式化验证,包括流程内部逻辑一致性的验证和是否满足用户需求的正确性验证,从而完成Web服务的设计时组合。本文最后提出了系统结构框架,以及原型系统的设计和实现。Web服务组合的系统框架从抽象的层面刻画了Web服务组合系统的主要组件、功能和过程。本文提出了基于SOFL的Web服务组合的系统框架WSCFBS(Web Service Composition Framework Based on SOFL),支持Web服务的设计时服务组合。基于WSCFBS,设计和开发了基于SOFL的Web服务组合的原型系统,实现了本文提出的Web服务发现,Web服务组合和Web服务组合验证方法。