模型检测是一种自动化系统验证技术,通过对系统形式化建模以及性质的形式化描述,采用搜索算法判断系统是否满足待测属性并给出可达路径或反例路径。然而,在实际应用中,许多系统的状态空间可能非常大,这使得验证所需的时间和消耗的资源会随着状态数的增加而呈现指数级的增长,这就是模型检测中的状态爆炸问题。该问题导致验证时间过长,检测效率低下,极大地阻碍了模型检测在工业界的应用和发展。为解决上述问题,本文提出了基于探针计算机的模型检测方法,实现了全并行的系统验证。该方法利用了探针机模型底层完全并行的特点,极大地减少了模型检测中图搜索算法的时间,解决了在图灵机上无法处理状态爆炸的难题。为此,本文将探针计算机数学模型应用于模型检测问题,构建了两者之间的映射关系,提出了时态逻辑（LTL）和计算树逻辑（CTL）并行验证方法,该方法扩大了系统验证规模,提升了检测效率。并以此开发设计了MC2PROBE模型检测器,将之应用到漏洞挖掘系统中,解决了对于大规模程序中的复杂漏洞自动化检测问题。最后,本文的主要贡献包括:（1）提出了基于CTL语义的模型检测映射算法,将Kripke结构转化为可以在现有探针计算机上运行的数据库和探针库,该方法只需一次图搜索就能找到系统中的所有反例,减少了针对大状态空间系统的验证时间。（2）提出了在线性时间内找到多个接受环的算法,设计了基于探针计算机的求解强连通分量方法,该方法可以有效减少求解CTL操作符EG和LTL模型检测的验证时间。（3）开发了MC2PROBE模型检测器,仿真了探针计算机的探针计算过程,检测器将系统模型作为输入,最终可以获得所有可行的路径或反例。在不同状态数的系统模型上进行了检测器的对比实验。与传统的模型检测器相比,实验结果证明了本方法的可行性和效率。（4）设计并实现了基于MC2PROBE的漏洞挖掘系统。该系统利用工具将二进制代码进行反汇编,在此基础上通过静态分析方法,实现了危险函数调用漏洞与循环读写漏洞的自动化挖掘。系统结合了MC2PROBE模型检测器的特点,解决了传统静态分析方法搜索覆盖率差,效率低的问题。