模型检测技术是一种可以实现对系统性质进行自动检测的技术，该技术自从被提出来之后，得到了广泛的关注，越来越多的模型检测算法和技术被提了出来。但现有的模型检测算法只能至多找出系统中的一个反例，随后便会退出搜索。因而并不存在一个算法可以一次性找出待测系统中的所有反例。于是，在本文中便针对该问题进行了研究，并提出了一个可以一次性搜索出系统中所有反例的并行完备模型检测算法。本文首先对模型检测技术的基础知识进行了介绍，并对当前模型检测技术的发展状况进行了总结。然后，对所提出的并行完备模型检测算法进行了详细的讲解。该算法可以在线性时间复杂度的情况下一次性找出系统中的所有反例。它是在深度优先搜索DFS的基础上实现对待测系统的状态空间进行搜索。其进行反例搜索的流程是首先并行的从接收状态开始，通过逆向转移关系搜索出系统中所有的接收环，再并行的从初始状态开始搜索出所有的从初始状态到达接收状态的路径，最后再运用这些结果进行反例的构造。在算法中，不仅采用了并行技术来加速对状态空间的搜索，与此同时，还运用了哈希函数来实现状态间的快速比较。当待测系统规模较大时，算法会采用磁盘进行状态的存储。如果系统中不存在接收环时，算法会立即终止，因为这意味着系统中并无反例存在，这可以缩短检测时间。在本文中，除了从三个方面对并行完备模型检测算法的正确性进行了理论证明，还从两个方面对算法的时间复杂度进行了分析，并与其他的并行算法进行了比较，显示了并行完备模型检测算法的优势。并在SPIN工具上实现了该算法，最终以实验的方式，证明了算法能够一次性找出所有反例的事实，并通过与原SPIN检测结果的比较，展现了算法不仅可以找出所有反例的优点，并且在对不具有反例的系统进行检测时，其搜索效率也较原SPIN的高。与此同时，还运用相应的实验数据对算法的效率进行了分析，并得出并行完备模型检测算法的时间复杂度与系统状态数是近似线性的。