Web服务可用来实现应用程序在互联网上的互操作,它已成为一种极具发展潜力的分布式网络应用集成技术。对组合服务的研究,不仅可以实现行业内服务的有效使用,也可以帮助行业服务拥有者将业务扩大化,提升业务价值。Web服务组合要实现的最终目的是希望能开发出高质量和满足用户需求的服务组合系统。而系统能否满足用户需求,本质上是由实际执行的具体行为所决定的,也就是说,执行行为的正确与否决定了系统能否满足用户需求。本论文从理论研究和实践结合两个方面着手,研究探索了服务组合的形式化建模、验证以及模型驱动的可视化技术。采用基于行为描述语言的建模方法,可以抽象化流程中的服务行为,这些行为是关系着不同的Web服务之间的通信和交互的,对建立的行为模型可以进一步进行相关特性的验证,这对后续组合服务能否正确执行并成功实现用户既定的目标提供了理论依据。在此基础之上进行的模型驱动的行为模型可视化的研究,可以实现让不同知识背景的用户更直观准确的掌握行为模型中复杂的行为交互,以保证后续开发过程的高效性和表达的准确性。本论文的主要工作如下：(1)建立了基于BPEL4WS的形式化服务组合行为模型WSBM,该模型以行为描述语言BDL为基础,给出了BPEL4WS到BDL的转换与建模方法。使用行为描述语言BDL可以建立一个形式化的行为模型,通过对BPEL4WS描述的Web服务组合系统与BDL模型进行分析和比较,能够将服务组合系统中的概念和元素与BDL模型中的概念和元素对应起来。由变换语义学的概念,这样建立起来的形式化服务组合行为模型WSBM继承了BDL的基本语法和语义。(2)构造出了形式化服务组合行为模型WSBM的模拟执行过程。在构造的过程中,从初始状态出发,通过追踪复合行为表达式的变化,得出WSBM形式化模型在每个状态下的迁移事件集合,并获得他们之间的映射关系,最终得到模型的运行轨迹。并给出了模拟执行模型的语义正确性证明,使用标记迁移系统作为其操作语义,描述了WSBM模型的状态演化过程,构造了一个等价的执行模型来描述行为模型的运行轨迹,对系统进行语义检查。(3)进行了Web服务组合形式化模型的特性分析验证。由于Web服务的可复用的概率非常高,因此一个组合服务如果在未经过验证以前就发布出去,一旦出现错误,付出的代价将会很大。因此在组合流程发布之前要对其进行验证。可以采用形式化建模与验证的方法,通过模型的语法以及语义规则来表示和建立需求模型及其执行模型,并通过对目标系统的特性分析,最终验证目标系统所能满足的相关特性。本文研究了Web服务组合的验证问题,提出了服务组合匹配性验证方法。该方法能够在服务部署前发现组合逻辑上潜在的行为不匹配性,从而提高了服务组合的健壮性和用户满意度。并且通过一个实际案例验证了本方法的正确性和有效性。(4)以web服务组合的行为模型驱动的组合行为交互表达的可视化方法。通过形式化建模和验证,系统的相关特性已经得到了保证。然而要让用户通过阅读和理解模型的语法甚至语义规则来了解需求模型仍然是一件困难的事情。一种较好的方法是采用可视化的技术,将模型形象地表达出来,使用户能够直观地认识和理解需求模型。本文通过对具体Web Service实例的形式化模型,转换为对其组合的可视化动画形式。在建立了组合服务行为模型后,首先使用模型转换的方法将行为模型转换成状态机,以作为需求动画的模型。再根据需要选择需求可视化描述的实体集,并选择对应的图形和图片以直观地表达所选择的实体。然后,根据所选择的实体集,利用状态抽取的方法从模型中提取该演示范围内与这些实体对应的状态块,并将每个状态块中的迁移与提供的动作原语进行关联,作为行为的可视化描述。当状态机执行时,驱动动画引擎根据状态块中对应的迁移,调用相关联的动作原语,控制与对象关联的图形运动,从而直观地表现出模型所描述的行为过程。