Web组合服务是一种基于面向服务的应用程序,它可以将多个异构的、跨平台的,不同开发者所开发Web应用程序加以组合,利用不同的逻辑控制流跳转,组成功能不一样的基于互联网的应用程序。在它产生以来,就引起了业界广泛的关注。而大规模的Web组合服务中由了很多异构的Web服务组成,它的控制流程很难得到保证,故本文利用模型检测的方法来验证大规模Web组合服务的系统安全性、可用性和验证其多主体认知逻辑。本文首先对相关的技术和基础知识做了介绍,并对当前学界对Web服务的模型检测验证研究现状进行了总结。接着本文将Web组合服务看做一个带有多主体的认知逻辑系统,并证明其可行性,给出BPEL语言中的活动的迁移元组。接着本文为了增强模型检测算法对于大规模系统的把控能力,更好地解决由于系统空间状态爆炸而产生的问题,引入了磁盘Mysql数据库对系统状态进行管理。通过对宽度优先状态搜索算法中,利用数据库减少每层计算机系统需要处理的模型系统状态。并且利用哈希算法,尽量减少算法的IO读取次数,在可接受的系统资源消耗的情况下,达到系统全空间状态搜索的目的,并返回系统所有可能的反例。最后本文根据日常生活中,电子商务的场景,构建出电子商务的交易模型,给出其Promela语言形式,并给出此模型的多主体认知逻辑到LTL的转化。并利于本论文提出算法的实现的模型检测器对交易模型的检测结果,与其他模型检测器(如Spin等)的检测结果作比较。本文从建模和算法实现的两方面入手,提出一种可以对大规模Web组合服务进行模型检测验证,并且能将其看做多主体系统,验证其认知逻辑属性的办法。从与其他模型检测算法的理论与实验结果的比较可看出,本论文提出的算法能找出模型中的所有反例,并且对于大规模系统的搜索效率也较其他模型检测算法高。与此同时,还可以成功验证Web组合服务多主体认知逻辑属性,充分体现了基于磁盘的宽度优先状态搜索算法的优势。