面向服务的计算SOC(Service-Oriented Computing)与面向服务的体系架构SOA(Service-Oriented Architecture)代表了分布式计算和软件开发的最新发展方向。Web服务组合是实现SOC & SOA的核心技术之一,它是一种基于Web服务协议组合已有Web服务、构建Web应用的软件构建新形态。由于被组合的Web服务是由不同组织发布、分布在Internet上、具有自治特征的软件组件,在开放、动态、难控的Internet环境下实现各类Web服务资源集成和共享的Web服务组合,其QoS(Quality of Service)成为影响其能否成功的关键因素之一。在系统分析和设计阶段,建立Web服务组合的模型并分析验证其功能正确性和QoS可满足性,是提高Web组合服务可信性的重要手段。目前,Web服务组合建模和验证的研究一般对功能和QoS分别进行建模和验证,由于需要分别建立功能模型和QoS模型,并且建立两者的阶段可能不同步,通过功能验证的系统模型可能并不满足QoS要求,需要重新进行设计或调整,从而增加了开发成本,同时延长了开发周期。造成这一问题的原因在于目前的建模、验证的方法、工具对Web服务组合功能和QoS统一建模和验证的支持不足,因此,有必要对现有建模、验证的方法、工具进行QoS扩展以支持Web服务组合功能和QoS统一建模和验证。为此,本文针对下述问题展开了研究:第一,由于Web服务的QoS涉及多个质量属性,且属性值的评估方法随应用领域和组织机构的不同差异较大,不可能把这些质量属性一一扩展进已有方法和工具,因此,如何从这些QoS属性中提炼出适合建模的属性进行扩展,如何以一致的方式对这些属性进行评估和比较,是Web服务QoS属性模型和评估问题。第二,UML序列图SD(Sequence Diagram)是一种使用广泛的用于描述系统组件之间交互行为的图形化建模语言,具有建模直观、易于掌握和使用的优点,容易为最终用户、需求分析人员和系统设计人员所接受。由于Web服务组合的一个显著特点是参与组合的Web服务之间的交互,因而SD适合于Web服务组合交互行为的图形化建模。然而,目前SD对QoS的建模支持不足,因此,如何对SD进行QoS建模扩展以支持Web服务组合的建模,是基于UML的Web服务组合QoS建模问题。第三,进程代数PA(Process Algebra)是适合于描述并发和组合系统、面向验证的形式化建模和分析语言,具有形式化的精确语义以及较丰富的自动分析验证的方法和工具,而Web服务组合的一个显著特点是参与组合的Web服务之间的并发和组合,因而PA适合于Web服务组合的形式化分析和验证。然而,现有PA对QoS的建模和分析支持不足,因此,如何对PA进行QoS扩展以支持Web服务组合的分析和验证,是基于PA的Web服务组合QoS分析和验证问题。第四,由于SD的语法采用图形符号表示,语义采用自然语言描述,缺乏形式化的精确语义,难以直接支持形式化分析与验证。而PA基于严格的数学基础,其语法和语义采用形式化符号表示,不易为最终用户、需求分析人员和系统设计人员掌握和使用。因此,在这两种语言进行了QoS建模扩展之后,如何提供一种方法来实现两者的转换,从而把这两种语言的优势融合在一起以支持Web服务组合建模和分析验证,是具有QoS特征的模型转换问题。本文通过系统研究上述问题,取得了如下主要研究成果:(1)提出了Web服务QoS抽象模型和评估方法。目前Web服务研究中关注的QoS属性较多,且属性值的评估方法随应用领域和组织机构的不同差异较大,不利于以一致的方式来评估Web服务的QoS。从抽象的角度,从众多QoS属性中提炼出时间、概率、代价三种抽象QoS属性。在此基础上,给出了QoS多属性归一化处理方法和多属性综合评估方法,支持在模型层面以一致的方式评估Web服务的QoS,以及QoS优化的Web服务选取。(2)提出了面向Web服务组合建模的QoS序列图SDQ(Sequence Diagram for QoS)。把时间、代价信息映射到UML基本序列图SD中,提出扩展了时间和代价建模能力的基本QoS序列图bSDQ(basic SDQ);把概率信息映射到高层序列图,提出了高层QoS序列图hSDQ(high level SDQ),支持把不同建模者创建的局部bSDQ概率合成为全局SDQ。在此基础上,给出了BPEL4WS活动到SDQ的映射,以及基于SDQ的Web服务组合建模方法,支持Web服务组合功能和QoS相统一的图形化建模。(3)提出了面向Web服务组合验证的QoS进程代数PAQ (Process Algebra for QoS)。针对现有PA对QoS分析验证支持不足的问题,把时间、代价、概率信息映射到PA中,给出了PAQ的语法和语义,证明了PAQ在PA基础上扩展了QoS分析验证能力。在此基础上,给出了基于PAQ的Web服务组合分析验证方法,支持Web服务组合功能和QoS相统一的形式化分析验证。(4)提出了SDQ到PAQ的转换方法。给出了SDQ的形式语法,以及基于PAQ的SDQ形式语义。在此基础上,给出了SDQ到PAQ的转换算法,支持SDQ到PAQ的转换,从而可以把SDQ图形建模和PAQ形式分析验证的优势结合起来。(5)基于上述方法,设计了Web服务组合统一建模和验证工具UMV4WSC (Unified Modeling and Verification for Web Services Composition),支持Web服务组合功能和QoS建模,支持图形建模和形式分析验证。在此基础上,给出了基于SDQ建模Web服务组合、SDQ模型转换为PAQ模型、PAQ模型分析验证的完整案例,实例分析说明了上述方法的有效性。