基于模型检验的测试用例生成方法研究

软件产品复杂度的不断增加和发布期的缩短给软件测试带来了严重的挑战，软件测试自动化是一种必然趋势。主要探索用模型检验的反例生成能力实现软件测试自动化的原理和关键问题；研究通用测试覆盖准则在基于模型检验的测试中的可应用性以及从测试覆盖准则自动生成陷阱性质的方法，通过模型检验陷阱性质产生的反例构造测试用例；研究不确定性模型带来的测试用例可控性问题，提出可控性问题解决方法；研究从安全性质产生测试用例的方法；结合组合推理原理和抽象精化框架，研究测试用例生成的抽象精化方法；研究集测试目标缩减、测试用例生成过程监控和测试包缩减于一体的测试优化方法；开发基于模型检验的测试用例生成工具，建立基于模型检验的测试自动化框架。基于模型检验的测试支持测试自动化，支持软件开发与测试的并行化。项目研究在学术上对软件测试方法、软件质量保证、软件过程改进和维护有重大意义，研究成果可以广泛应用到软件产品的开发过程。

软件产品复杂度的不断增加和发布期的缩短给软件测试带来了严重的挑战，软件测试自动化是一种必然趋势。主要探索用模型检验的反例生成能力实现软件测试自动化的原理和关键技术。.提出了产生数据流覆盖和状态图覆盖准则（状态覆盖、迁移覆盖和迁移对覆盖）的时态性质的形式化方法，给出了提取时态性质的方法；基于危险迹概念，提出了安全性质测试的建模方法和基于图结构覆盖的安全性质测试准则；结合反例引导的抽象精化框架和组合验证方法，组合抽象构件产生构件组合的抽象模型，从抽象模型生成抽象测试用例，利用反例引导的抽象精化框架产生具体的测试用例。提出了构件组合的测试生成抽象精化方法；利用测试目标排序、时态逻辑公式重写等技术，提出了一种基于模型检验的测试生成过程的on-the-fly监控优化方法，实现测试目标和测试包的动态约简，降低测试冗余；基于FSM模型的测试方法及其相关理论，提出测试序列集合冗余约简方法、FSM测试的评估量化指标、以及最小测试成本迁移覆盖准则和准则的充分必要条件，设计了最小测试成本迁移覆盖的实现算法，对若干基于FSM模型的测试方法进行了实验评估；在软件特别是对Web应用和Web服务的形式建模和验证方面进行了重点研究，除了定性检验，还关注定量验证。使用概率对现有的形式模型如Petri网进行扩展，定义了其代数语义和逻辑语义，开发了非确定概率系统的建模、分析、模拟和验证技术。.开发了基于模型检验器NuSMV的测试生成算法，建立了一个基于模型检验的测试生成自动化框架。框架集成了NuSMV、UML建模工具ArgoUML、以及从FSM到NuSMV程序的自动化转化工具、性质辅助描述工具和反例解析工具等；开发了一个集模型转换器、测试目标分析器、测试序列生成器、以及测试执行引擎等功能的基于FSM的测试工具原型；提出了基于SOA的模型检验工具集成体系结构，无需本地安装和配置模型检验工具，实现了模型检验的远程透明访问。.基于模型检验的测试支持测试自动化，支持软件开发与测试的并行化。研究成果可以广泛应用到软件产品的开发过程。