随着计算机技术的快速发展，计算机软硬件系统的规模也急速增大，系统中会出现较多的错误和设计缺陷，这给系统的可靠性验证带来较大的难度。此外，一些安全攸关的系统（如电子商务系统、医疗仪器、以及汽车、飞机的控制系统等）在人们生活中也被广泛地应用，即使很小的设计缺陷或程序错误也会带来巨大的财力、物力损失甚至危及人们的生命安全。因此，如何保证系统的正确性和可靠性成为日益紧迫的问题。　　 形式化验证技术凭借其数学和逻辑的严谨性，提供了一种验证系统正确性和可靠性的方法。作为其中的一种形式化验证技术，模型检测技术以其自动化程度高得到了人们的广泛关注和认可。然而，模型检测技术也面临“状态空间爆炸”问题的挑战。针对这一问题，一些研究人员提出了符号模型检测技术、偏序规约、对称规约以及限界模型检测技术等以缓解状态空间爆炸问题。为了应对状态空间爆炸问题，研究人员也提出了一种基于假设检验和随机抽样的MonteCarlo模型检测技术。该技术是一种带单边误差的随机化算法，属于基于自动机理论的线性时序逻辑(LTL-LinearTemporalLogic)模型检测。算法运行速度快、节省内存，而且具有很好的可扩展性。然而，该算法采用均匀分布的随机搜索不一定非常高效地寻找到反例。因此，本文提出了一种新颖的结合带赋值符号迁移图和启发式搜索的MonteCarlo模型检测算法，实现了基于该算法的验证工具，并使用几组程序实例进行了原MonteCarlo模型检测算法和本文提出的基于带赋值符号迁移图的MonteCarlo模型检测算法的对比实验。实验结果表明，将带赋值符号迁移图和表示性质公式否定式的自动机合成乘积Btüchi自动机，并在其上执行有导向的随机搜索的启发式算法有效可行，提高了寻找反例的效率，显著地减少了在状态空间上搜索的状态数量，从而缓解状态空间爆炸问题，提高模型检测的性能。