模型检测技术是最近二十年来最成功的自动验证技术之一，目前已经被广泛地应用于有穷状态系统(包括电路设计和通信协议)的分析与验证。由于这一技术是基于对状念空间的穷尽搜索，“状态爆炸”问题一直是制约其在实际系统中应用的主要技术瓶颈。 对于大规模系统，由于受到内存空间的限制，模型检测技术往往难以完成对系统状态空间的穷尽搜索，而一般的随机搜索算法对于寻找系统中可能存在的错误的搜索效率极低。为了在时空效率方面取得一个较好的平衡点，本文提出了一种基于启发式信息的解决方案，其要点为：以Kripke结构为并发系统的模型，使用线性时序逻辑LTL来描述系统所期望的性质，将该公式取反后得到反例路径的LTL公式；通过计算一条路径满足的该公式的最大结构复杂度，我们判定所采集的路径在多大程度上“符合”所描述的反例特征，由此实现对搜索方向的引导。通过类似遗传算法的搜索流程，我们期望能够尽快的找到可能存在的错误。实例研究表明，对标准的模型检测工具无法处理的大型系统，本文所提出的方法能以较好的概率发现隐藏的错误，并给出相应的诊断信息。 论文的主要工作如下： · 设计了基于LTL路径公式的启发式信息，以及选择，交叉，变异等进化操作。 · 根据所设计的启发式搜索算法，实现了相应的原型工具。 · 通过实例研究证明了算法的有效性。