面向服务的体系结构(Service-Oriented Architecture, SOA)是分布式计算和软件开发的最新发展方向。SOA的目的是以Web服务为基础，有效地解决在分布、动态、异构环境下分布式应用集成问题。Web服务作为一种自治的、与平台无关的网络化构件，具有松耦合、支持动态组合和重配置等特点，从而为Internet环境中软件开发和分布式应用提供了新的技术。　　 通常，将多个服务动态地组合成一个新的组合服务以满足用户的需求。描述这种组合过程的Web服务组合描述语言主要是WS-BPEL(Web Service Business Process Execution Language)和WS-CDL(Web Services Choreography Description Language)，这些语言存在两个方面的缺陷：一是，由于这些语言都是基于XML的，缺乏建模的理论基础；二是，这些语言未能提供验证其规约正确性的方法。　　 考虑以上问题，不仅要保证在设计阶段Web服务组合规约的正确性，还要保证在运行时阶段Web服务组合规约的正确性，所以本文系统地研究了Web服务组合建模、静态验证和动态验证三个方面，主要研究成果如下：　　 (1)研究了Web服务组合建模的问题，提出了一种基于UML模型的Web服务编舞语言WS-CDL建模方法。采用UML构件图表示WS-CDL的结构模型，用UML顺序图来建立WS-CDL中各个角色之间的活动模型，并自动地从顺序图中生成UML状态机图模型来表示单个角色的行为模型，并从WSDL规约中获得WS-CDL的数据流信息，用UML类图来表示数据流。该方法提供了图形化的前端，方便了设计者直接建立服务组合模型，并考虑Web服务组合过程中数据流的建模问题。　　 (2)研究了Web服务组合的静态验证问题，提出了一种基于UML模型的WS-CDL的模型检验方法。该方法将UML模型表示的WS-CDL转化为Cadence SMV模型检验工具的输入，并验证系统模型是否满足规定的属性。该方法不仅能够验证Web服务组合过程中的结构属性和行为属性，而且能够验证数据属性。实验结果表明，该方法能够验证中等规模的带数据的Web服务组合中的关键属性。　　 (3)研究了运行时Web服务组合过程中时态属性的动态验证问题，提出了一种基于PSC的Web服务组合过程中时态属性的监控方法。引入了属性序列图(Property Sequence Chart, PSC)，定义了PSC的形式语法和语义，采用运行时监控技术来持续地监控Web服务组合过程的执行轨迹是否满足PSC表示的时态属性。实验结果表明，该方法能够有效地检测运行时Web服务组合过程中存在的时态错误。另外，由于PSC图形化的优点，使得表示时态属性简单、易于理解，从而解决时态逻辑表示时态属性复杂和不够直观的问题。　　 (4)研究了运行时Web服务组合过程中时间属性的动态验证问题，提出了一种基于TPSC的Web服务组合过程中时间属性的监控方法。鉴于PSC图形化的优点，将PSC扩展为TPSC(Timed PSC)来表示时间属性，给出了基于时间Büchi自动机的TPSC操作语义，并用实时规约模式来评估TPSC的表达力。采用运行时监控技术检测Web服务组合过程的执行轨迹是否满足TPSC表示的时间属性，并采用基于假设检验的统计技术对这些时间属性在运行时成立的概率进行计算。实验结果表明，该方法能够在运行时精确地监控时间属性成立的概率，并具有良好的性能。　　 (5)设计和实现了两个原型工具T-WS-CDL和WS-PSC Monitor，以支持以上提出的理论和方法。T-WS-CDL实现了基于UML的WS-CDL建模方法和静态验证方法。WS-PSC Monitor实现了基于PSC的时态属性监控方法和基于TPSC的时间属性监控方法。