模型验证是一种重要的自动化验证技术。给定一个软件或者硬件模型和相应的安全性质,模型验证技术可以自动化地验证模型是否安全,从而保证软件或者硬件系统的可靠性。该技术自提出以来就受到了广泛地关注,并很快被工业界应用在了实际的硬件设计及软件开发中,相应的模型验证工具也如雨后春笋一般层出不穷。然而,除了大型企业会为它们的特别需求设计专门的模型验证工具之外,在普通的硬件设计和软件开发流程中,模型验证技术的普及程度还远远不够。造成这种情况的原因有许多,其中一个非常重要的原因是,开源模型验证工具的成熟度还达不到实际应用的要求。在实际使用中,开源模型验证工具的使用者常常会遇到诸如正确性缺陷、工具崩溃以及工具可用性不高等问题的困扰。造成这些问题的原因是,对于模型验证工具,没有针对性、系统性并且有效的测试方法。目前开发者仅通过在有限的测试样例来验证模型验证工具的可靠性,很明显,这是远远不够的。针对这一问题,本文系统性地提出了一套针对模型验证工具链的模糊测试方法,以提高软件模型验证工具的可靠性,推动模型验证技术的普及。模糊测试是一类自动化生成随机测试用例的方法,此类方法已经在多种软件的自动化测试上取得了很好的效果。然而,将模糊测试应用在模型验证工具测试中,仍存在以下几个难点:第一,如何自动化地生成符合模型验证工具链输入规范的测试输入;第二,如何自动化地获得生成的测试输入的预期输出;第三,同样也是最重要的一点,如何在模型验证工具链中找到真实的缺陷。本文针对这三个难点,提出了下列针对模型验证工具的模糊测试方法以及相应的测试工具:·电路结构变异:硬件模型检查器是针对硬件电路的模型验证工具,而电路结构变异则是一种针对硬件模型检查器的模糊测试方法。它的核心思想是,通过随机改变已有电路图中的电路连接方式,从而构造出新的符合硬件模型验证输入规范的测试输入。基于电路结构变异,本文实现了一款叫做AIGMutator的测试工具,它在目前最好的三个硬件模型检查器中找到了9个不同的软件缺陷。·可达性问询:软件模型检查器是针对软件程序的模型验证工具,而可达性问询是一种针对软件模型检查器的模糊测试方法。它的核心思想是,通过实际执行获得程序分支的可达性,然后将可达性合成已知的安全性质,再将程序与已知的安全性质作为软件模型检查器的测试用例。基于可达性问询,本文实现了一款叫做MCFuzz的工具,它在目前最好的三个软件模型检查器中找到了62个不同的软件缺陷。·语义融合:SMT求解器是模型验证工具中重要的核心部件,而语义融合是一种针对SMT求解器的模糊测试方法。该方法的核心思想是,将两个有着相同可满足性的SMT公式融合成一个新的公式,同时保持新公式的可满足性不变,之后将新公式作为SMT求解器的测试用例。基于语义融合,本文实现了一款叫做YinYang的工具,它在最好的两个SMT求解器中找到了45个不同的软件缺陷。·类型感知变异:类型感知变异同样也是一种针对SMT求解器的模糊测试方法。它主要将SMT公式中的操作符变异为类型合法的新操作符,从而生成新的公式,并将新公式作为SMT求解器的测试用例。基于类型感知变异,本文实现了一款叫做OpFuzz的工具,它在最好的两个SMT求解器中共找到了1092个软件缺陷。这些方法不但解决了模型验证工具难以有效测试的难题,同时也为软件测试方法论提供了新的思路。除此之外,本文实现的工具不仅在模型验证工具测试方面取得了很好的效果,同样在其他领域和用途上也具有广泛的应用前景。