随着多核心处理器系统的发展,分布式并发系统已成为当前主流的软件体系结构。分布式软件的特性导致错误不可重现,使软件排错工作非常困难。Java是在语言级别支持并发的高级语言,其提供的语言特性和大量的类库很好地支持了并发程序的编写。但这些类库都有各自的特点,如果使用不当会造成一些难以发现,却危害严重的问题。同时,Java内存模型JMM(Java Memory Model)允许编译器在优化过程中改变程序的执行顺序,这会让多线程Java程序产生许多意想不到的错误。Java规范中程序的正确性仅仅依赖于程序员编写正确的,不会冲突的代码,很难满足高可靠性软件的要求。针对上述问题,本文提出了一套对Java多线程并发程序错误进行检测的方法。第一部分工作提出了一种自动化模型检测的技术,并制作了工具JTS(Java To SPIN),实现了对Java并发程序的模型检测与验证。JTS对Java程序进行分析,产生抽象语法树,建立程序的抽象模型。分析中特别针对Java虚拟机的并发机制和类库实现进行了建模,并利用模型检测工具SPIN进行了模型检测。在实验中JTS成功地对多个Java程序进行了模型提取和模型检测,给出了错误路径。JTS建立的模型准确地再现了Java程序的执行过程,发现了其中隐藏的并发程序错误。这种检测方法为发现和修正这类不可重现,难以测试的并发错误提供了一种新的方法和思路,是传统测试方法在并行程序领域的的一种尝试与补充。第二部分工作提出了另一种新的方法,针对JMM所允许的程序顺序变化,结合程序中的依赖关系、volatile变量和串行化代码等建立模型,进行模型检测。根据这种检测方法,给出了程序的乱序模型和模型检测结果。在模拟执行和检测结果序列中,可以清楚地看到Java多线程并发程序的乱序执行情况。该方法检测现有JMM规范下所有允许的代码顺序变化,可以发现原有技术无法检测的错误,并给出错误路径,推进了高可靠性Java程序的验证工作。