随着Web服务技术的不断发展,Internet上的服务的数量快速增长。一般来说,具有单一功能的原子服务往往不能灵活地应对复杂的要求,那么将两项或更多项服务结合在一起变得越来越重要。但是,在复杂和动态的网络环境中,很难保证Web服务组合过程的正确性,另外Web服务组合过程还会有一些别的非功能的属性要求,同时在Web服务组合中会存在概率时间方面的信息,所以对Web服务组合进行量化验证是极为重要的。为了实现Web服务组合的量化验证,本文所做的工作如下:(1)对业务过程执行语言BPEL(Business Process Execution Language)中的基本组成元素基本活动和结构化活动进行分析,提出使用Web服务组合-扩展迁移系统WSC-XTS(Web Service Composition-Extended Transition System)对BPEL过程中的基本活动和结构化活动进行形式化建模。并且给出BPEL转化为WSC-XTS模型的算法和迁移图表示,其中,算法给出了 BPEL到WSC-XTS模型的具体步骤,而迁移图可以形象地表示如何转化。(2)用概率模型检测器 PRISM 中的 CTMC(Continuous-Time Markov Chain)模型对该WSC-XTS进行描述和验证。文中给出常用的一些属性描述方式,并通过一个处理采购订单的服务组合例子进行了相关分析。(3)当Web服务组合不满足需求时,需要根据反例重新选择Web服务进行组合。本文综合比较了两种已有的反例产生算法 KSP(K-Shortest Path)和 XBF(Extended Breadth-First)算法,提出了一种结合了两者优点的反例产生方法XSP(Extended Shortest Path)算法。算法XSP采用算法KSP产生一条诊断路径,并采用算法XBF的图存储该诊断路径,该算法避免了算法KSP需遍历路径以及算法XBF产生次优路径的缺点。