Web服务是一种面向服务计算的应用。不同的开发商通过使用不同的逻辑控制流将异构、多平台的Web服务组合成一个新的Web服务,称之为Web组合服务。Web组合服务控制流的安全性很难得到保障,本文的目的就是解决Web组合服务控制流的安全性。本文把Web组合服务看作是多主体系统,使用基于条件转移的模型检测方法对Web组合服务验证,这种模型检测方法以构建条件转移系统为基础。基于条件转移的模型检测方法分为基于动态建模方法的动态检测方法和基于静态建模方法的静态检测方法。基于条件转移模型检测方法的核心思想是根据规则集产生系统的状态集以及转移关系集合,动态检测方法在建模效率以及错误定位效率方面有很好的优越性,本文采用动态检测方法对Web组合服务验证。状态爆炸是模型检测过程中始终存在的问题,对于大规模的Web组合服务,状态爆炸问题依然存在,本文采用基于外存的条件转移模型检测方法解决该问题。本文结合宽度优先搜索算法和基于外存的思想提出了基于外存的条件转移模型检测算法,该算法使用条件转移模型检测方法的思想并对新产生的一层数量巨大的状态进行分块操作,该方法缓解了内存的压力,使得模型检测器验证大规模的系统成为了可能。本文给出了Web组合服务的规则集和根据规则集产生的Web组合服务的条件转移系统,并对Web组合服务的反例路径进行分析。本文改进模型检测器NuSMV并使用改进的模型检测器对Web组合服务验证,然后与其它的模型检测器(Spin,NuSMV等)进行实验对比,得出基于条件转移的模型检测方法具有验证更大规模Web组合服务安全性的能力。