随着互联网技术的迅速发展,传统的分布式计算技术已不能满足用户需求,Web服务应运而生并成为面向服务计算的范例。随着Web服务技术的不断发展及其应用范围的逐步扩大,越来越多的企业将其业务功能和流程封装成标准的Web服务发布到Internet上,致使Internet上的服务数量呈指数增长的趋势。这些由Web服务提供者发布的Web服务中,存在大量功能相同但具有不同服务质量(QoS)的服务。这些日益增多的Web服务有成千上万种不同的组合方案,可以组合出具有相同功能但不同QoS的组合服务。如何判断服务组合方案是否满足用户的需求,是Web服务组合必须解决的一个关键问题。本文从提高QoS属性验证的准确度方面对Web服务组合QOS属性验证问题进行了探索性研究。首先,综合分析现有QoS模型的优缺点,提出了一种QoS本体模型,该模型以OWL-S为参考,对其中的过程模型进行了扩展,支持多种QoS属性的度量方式,能很好地满足服务质量描述的需求,具有良好的扩展性。其次,提出一种扩展OWL-S描述的Web服务组合模型转换为Markov模型的方法,并将Markov模型转换为概率模型检测器PRISM的输入语言,该方法能够实现自动验证基于扩展OWL-S描述的Web服务组合的QoS属性。最后,综合比较了两种已有的反例产生算法KSP和XBF算法,提出了一种结合了两者优点的反例产生方法XKSP算法。该算法采用KSP算法产生一条诊断路径,采用XBF算法中的Diag图存储该诊断路径,该算法避免了KSP算法需大量枚举路径的缺点以及XBF算法中产生次优路径的缺点。