基于B/S模式的Web应用既保留了C/S模式分布计算的特性，又便于集中管理，而且最重要的是对客户端的限制较少，因此极大地促进了Web应用的广泛使用。Web应用已经对商业、工业、财政、教育、政府和娱乐及人们的工作和生活产生了深远的影响。如何保证Web应用的正确性和可靠性得到业界的广泛关注。 Web应用的验证是一个较新的研究领域，由于Web应用的异构、分布、并发和平台无关等特性，使得对其验证比较困难。论文使用抽象技术来解决状态爆炸问题，引入“反例引导的抽象精化”框架，试图实现模型检验的自动化。 首先，研究模型检验技术，考察时态逻辑公式的特点。使用接口自动机对Web应用进行建模，通过接口自动机的组合来表达Web应用构件的组合。模型检验器的验证结果表明组合模型在验证中的效率要优于未组合模型，但组合模型有可能会存在状态空间爆炸问题。 其次，分析了状态爆炸问题，以及解决该问题的常见方法，给出了一种将组合和抽象相结合的方法。改进了“反例引导的抽象精化”框架，针对多构件Web应用，通过构造抽象模型的组合来构造组合模型的抽象。设计了抽象算法、组合算法、转换规则、反例确认算法和抽象精化算法。 最后，根据设计的算法，开发了一个基于“反例引导的抽象精化”框架的、图形化的Web应用模型检验辅助工具原型，自动解析用XML格式存储的模型集和待验证的性质，完成抽象、组合、转换和验证等功能。当伪反例出现的时候，自动进行抽象精化操作，并在控制台输出相应的验证信息，实现了Web应用验证的自动化。