在服务质量(QoS)感知的Web服务组合研究中,衡量服务质量的标准通常是用户的非功能属性。然而,传统的Web服务组合方法难以恰当地处理用户非功能属性的不确定性与多目标性,也并没有考虑环境的动态变化对Web服务组合过程的影响以及不同抽象服务之间的依赖性。针对以上问题,本文提出了一系列基于概率模型检测的Web服务组合验证方法。首先,针对用户的非功能性属性的不确定性与多目标性,提出一种基于概率模型检测的Web服务组合多目标验证方法,将用户非功能性属性建模成为多目标时序逻辑公式,将Web服务组合过程建模为定量多目标马尔可夫决策过程,使用概率模型检测工具验证。其次,环境的动态变化会影响具体服务的QoS值,因此,选择具体服务时应考虑环境对其QoS值的影响。针对此问题,在以上多目标验证方法的基础上,提出一种开放环境下的Web服务组合多目标验证方法。将环境的动态变化过程建模为马尔可夫决策过程,使之与Web服务组合的定量多目标马尔可夫决策过程交互,使用概率模型检测工具验证。再次,针对环境动态变化过程的随机性和Web服务组合过程中不同的抽象服务之间的依赖问题,提出一种基于参数化模型的Web服务组合验证方法。该方法将环境模型中不同状态之间的转换概率参数化以处理环境变化过程的随机性。同时,引入限制要求约束Web服务组合过程,以处理抽象服务间的依赖问题,同时有效地缓解了验证过程中的状态爆炸问题。基于以上方法,本文对“在线购物服务”,“交通服务选择”两个场景进行案例研究,证明上述方法的正确性和可扩展性,并给出定量分析结果。