中文摘要：

测试用例多样性是近年来提出的适应性随机测试的基本原理。其出发点在于软件输入域上导致错误发生的区域往往是毗连的。通过选择多样化测试输入，使之比较均匀地分布在软件输入域上，可以显著地提高随机测试方法的效率和错误发现能力。并发软件也存在类似的现象，即并发软件错误不是仅发生在单个的状态或迁移上，而是也常常表现在由连续状态变迁构成的子状态空间上。基于模型的测试是一类典型的并发软件测试方法，但由于状态空间爆炸问题，测试用例生成和选择一直是并发软件测试领域的研究难点。目前，测试用例多样性在并发软件测试方面还鲜有涉及。该项目将把测试用例多样性原理引入基于模型的测试方法中，探讨并发软件测试用例的多样性度量，以使测试用例的生成和选择能够比较均匀地覆盖系统状态空间；并进一步结合实例研究，考察多样化测试用例对并发软件测试效率和错误发现能力的影响，提出有效的并发软件适应性测试方法，并开发相应的自动测试平台。

结论摘要：

本项目结合模型检测与测试方法，从测试用例多样性的角度探讨并发软件状态空间的有效覆盖。项目研究工作以并发软件的组合模型检测和适应性随机测试两条线索展开。在组合模型检测方面，提出正确且完备的假设-保证（Assume-Guarantee）推理规则，使对并发系统可达状态空间的覆盖能够建立在对系统各组成模块进行局部分析的基础上。实例研究表明，该方法可以证明任意大小、任意有界拓扑且在任意初始状态下并发系统的安全性。提出“行为约束传播”思想，根据并发系统各组成模块之间的依赖关系来约简并发系统各组成模块的不可达状态，并相应开发了并发系统状态空间约简软件。实例研究表明，该方法能够缓解状态空间爆炸问题，提高模型检测和并发测试方法的可扩展性。在适应性随机测试方面，在调研并发软件测试研究发展趋势的基础上，调整了项目计划书中以基于模型的测试为基准的研究框架，直接以多线程并发程序为主要研究对象，使本项目能够更好地与实际应用相结合。基于idiom覆盖度准则，提出了面向多线程并发程序的适应性随机测试方法。实验结果表明，该方法能够提高随机测试方法的效率和错误发现能力，不论在完成测试所需的总体时间，还是在发现第一个并发错误所需的测试时间上，我们提出的测试方法都优于随机测试。提出了弱内存模型活动边界（active frontier）随机测试方法，避免了原基于物理时间序方法的可能误判，并相应开发了内存模型动态验证工具，发现了工业级龙芯众核处理器Godson-T的若干设计缺陷。本项目研究已基本达到预期目标，相关成果发表在国际期刊《International Journal of Foundations of Computer Science》、国际会议International Symposium on Automated Technology for Verification and Analysis（ATVA 2014）。并发系统状态空间约简软件获得计算机软件著作权登记证书（登记号2014SR095741）。本项目共计培养硕士研究生3人。后续在总结成果的基础上，将完成学术论文1-2篇，并指导研究生按时完成学位论文答辩。