Java并發(fā)程序的模型提取與模型檢測技術(shù)研究.pdf

1、隨著多核心處理器系統(tǒng)的發(fā)展，分布式并發(fā)系統(tǒng)已成為當前主流的軟件體系結(jié)構(gòu)。分布式軟件的特性導致錯誤不可重現(xiàn)，使軟件排錯工作非常困難。Java是在語言級別支持并發(fā)的高級語言，其提供的語言特性和大量的類庫很好地支持了并發(fā)程序的編寫。但這些類庫都有各自的特點，如果使用不當會造成一些難以發(fā)現(xiàn)，卻危害嚴重的問題。同時，Java內(nèi)存模型JMM（Java Memory Model）允許編譯器在優(yōu)化過程中改變程序的執(zhí)行順序，這會讓多線程Java程序產(chǎn)生許

2、多意想不到的錯誤。Java規(guī)范中程序的正確性僅僅依賴于程序員編寫正確的，不會沖突的代碼，很難滿足高可靠性軟件的要求。 針對上述問題，本文提出了一套對Java多線程并發(fā)程序錯誤進行檢測的方法。第一部分工作提出了一種自動化模型檢測的技術(shù)，并制作了工具JTS（Java To SPIN），實現(xiàn)了對Java并發(fā)程序的模型檢測與驗證。JTS對Java程序進行分析，產(chǎn)生抽象語法樹，建立程序的抽象模型。分析中特別針對Java虛擬機的并發(fā)機制和類

3、庫實現(xiàn)進行了建模，并利用模型檢測工具SPIN進行了模型檢測。在實驗中JTS成功地對多個Java程序進行了模型提取和模型檢測，給出了錯誤路徑。JTS建立的模型準確地再現(xiàn)了Java程序的執(zhí)行過程，發(fā)現(xiàn)了其中隱藏的并發(fā)程序錯誤。這種檢測方法為發(fā)現(xiàn)和修正這類不可重現(xiàn)，難以測試的并發(fā)錯誤提供了一種新的方法和思路，是傳統(tǒng)測試方法在并行程序領域的的一種嘗試與補充。 第二部分工作提出了另一種新的方法，針對JMM所允許的程序順序變化，結(jié)合程序中的