随着计算机软硬件系统日益复杂,如何保证其正确性和可靠性成为日益紧迫的问题。各国研究人员为解决这个问题付出了巨大的努力,并取得了很大的进展。在提出的诸多理论和方法中,模型检验以其简洁明了及自动化程度高而引人注目。模型检验利用面向系统的某类性质来检查它是否满足规约,在系统不满足所要求的规约条件时,算法会产生一个反例说明不满足的原因,它与测试有异曲同工之处。　　论文针对状态空间搜索,对模型检验和测试相结合的方法进行了深入研究,并提出了相应的改进算法,通过这些算法不仅保证系统的正确性和可靠性,而且改进了状态空间复杂度问题。　　论文的主要工作如下:　　(1)结合模型检验对测试技术进行了研究,提出了测试结构和产生测试用例的方法。通过它可进一步保证系统的正确性和可靠性。　　(2)根据符号化状态图的思想,对FSM转化为OBDD的方法进行了研究,提出了具体的转化算法。　　(3)对图搜索的非启发式和启发式算法的复杂度及其相互关系进行了深入研究,提出了相应的改进要点。　　(4)通过对传统的A*算法的研究,给出了基于传统算法相对应的BDDA*算法,降低了内存的使用率,进而解决了状态空间过大的搜索问题。