Internet的普及以及分布式计算、基于构件的开发和Web Services等技术的迅速发展和应用使Web应用渗透到国计民生的各个领域。Web应用的质量将直接影响人们的生活和工作。验证与测试是保证软件质量的最基本和最重要的手段。然而,Web应用是一种具有多层结构的分布式系统,异构性、动态性、连接的多样性和控制流程的可变性等特性给Web应用的验证和测试带来了严峻的挑战,必须改进传统的或提出新的验证和测试方法以适应Web应用的新特性。模型检验是一种自动化的、基于模型的性质验证方法,广泛应用于有限状态系统的自动验证。它通过有效地搜索有限状态模型的整个状态空间判定性质是否得到满足,在系统不满足性质时提供的反例可以用于诊断系统的错误。测试的目的在于发现系统的实际行为与预期行为是否存在不一致。传统的手工测试是低效的、易出错的、盲目的和不可再生的,并且受制于测试工程师的创造力。应用模型检验技术实现测试的自动化是当前的一个研究热点。使用模型检验自动生成测试用例的关键在于构造能使模型检验器输出反例的陷阱性质,然后从反例构造测试用例。论文以模型检验器SMV为形式验证工具,主要研究在模型检验的统一框架下Web应用的形式验证和功能测试方法。Web应用客户端的功能主要体现在它的导航行为,Web应用的质量的一个重要方面是导航行为的一致性和安全性。论文给出了用对象联系图描述导航相关对象以及对象间联系的结构建模方法,提出了用Kripke结构进行导航的行为建模的形式化方法并分别从验证角度和测试角度定义了导航行为与对象联系图之间的一致性关系。在此基础上,提出了基于模型检验的导航行为的一致性验证方法和一致性测试方法,设计了从Kripke结构到SMV程序的转换算法,并分别实现了导航行为的验证原型与测试原型。此外,根据常用的导航安全策略,给出了导航行为的安全性验证方法。Web应用服务器通过构件的组合提供业务逻辑和应用服务,形式验证构件组合的行为是保证Web应用质量的一个有效手段。针对构件组合验证的状态爆炸问题,论文结合组合推理和反例引导的抽象精化思想,提出了组合式的抽象精化方法并设计了相应的检验算法,使构件组合的模型检验转化为各成分构件的局部抽象精化。提出并证明了组合确认定理,使构件组合上的反例确认转化为各构件上的反例投影确认。构件组合的一个验证问题是组合行为是否隐含了不安全的行为?论文提出了一种新的描述构件交互行为的模型:构件消息自动机。基于监控理论的可控性概念,设计了一个验证构件组合行为安全性质的算法。对象(网页或构件)是Web应用导航和构件组合的基础。结合模型检验技术和数据流测试准则,论文提出了Web应用对象的自动测试生成方法。在对象的源代码不可用的情况下,对象的动态状态行为用对象状态机建模,然后被转换为描述控制流和数据流信息的对象流图。提出了基于数据流测试准则的陷阱性质生成方法,通过在对象流图上模型检验这些陷阱性质自动产生对象的数据流测试用例,实现了一个基于模型检验的对象数据流测试原型。用模型检验自动产生测试的一个缺陷是模型检验往往会产生大量冗余的反例。为此,论文提出了一种on-the-fly测试优化方法并设计了优化算法。当模型检验产生一个新反例时,一方面用新反例检测未检验的性质以消除冗余性质,另一方面比较现有测试集以消除冗余测试。