摘要：JPF是NASA开发的Java程序模型检测工具。该文通过改写JPF内核中生成状态空间的模块，使待检测程序在受监控状态下模拟执行。用Data-Race算法收集警告信息，引导程序模型检测工具只对死锁相关线程进行模型检测，避免了状态空间爆炸，实现了对大规模并行程序部分线程死锁问题的模型检测。利用启发式搜索算法，在不同的搜索深度赋给待执行线程不同的权值，进一步优化了模拟执行结果。