基于符號計數(shù)器抽象的并發(fā)布爾程序驗證研究.pdf

1、隨著計算機技術(shù)的快速發(fā)展和應(yīng)用需求，多線程并發(fā)程序成為現(xiàn)代程序設(shè)計的重要目標。由于線程之間的相互交錯執(zhí)行，可能會產(chǎn)生許多難以發(fā)現(xiàn)的微小錯誤，因此，并發(fā)軟件驗證成為備受關(guān)注的研究領(lǐng)域。然而，模型檢測并發(fā)軟件面臨嚴重的狀態(tài)空間爆炸問題，即可達狀態(tài)數(shù)隨著并發(fā)線程的增加而呈指數(shù)增長，對并發(fā)軟件直接采用模型檢測方法進行驗證的效率非常低，甚至無法在實際應(yīng)用中實現(xiàn)。
　　推動模型檢測發(fā)展的一個有效方法是謂詞抽象，對源程序?qū)嵤┲^詞抽象技術(shù)產(chǎn)生布爾

2、程序，布爾程序作為軟件驗證的常用模型，雖縮減了狀態(tài)空間，但仍是謂詞抽象精化技術(shù)的瓶頸。為解決狀態(tài)空間爆炸問題，本文圍繞并發(fā)布爾程序的線程狀態(tài)的可達性問題進行分析，為其提出了一些算法，并以一組布爾程序基準測試集證明了算法的有效性。主要工作與貢獻如下：
　　（1）研究了帶有有界線程創(chuàng)建的非遞歸并發(fā)布爾程序的可達性問題，結(jié)合on-the-fly技術(shù)提出了一種基于符號計數(shù)器抽象的判定方法。在計數(shù)器抽象方法中，計數(shù)器記錄每個局部狀態(tài)的執(zhí)行線

3、程數(shù)，由其構(gòu)成的向量表示系統(tǒng)的全局狀態(tài)。然而，在實際應(yīng)用中，難以實現(xiàn)為每個局部狀態(tài)引入一個計數(shù)器。本文的方法是僅為可達的局部狀態(tài)引入計數(shù)器，同時在全局狀態(tài)中保留局部狀態(tài)至少有一個線程執(zhí)行的計數(shù)器,去掉零值的計數(shù)器及其對應(yīng)的局部狀態(tài)，從而節(jié)省大量的存儲空間。
　?。?）研究了帶有無界線程創(chuàng)建的非遞歸并發(fā)布爾程序的可達性問題，在上一個方法的基礎(chǔ)上進行了擴展，提出了一種基于Karp-Miller可覆蓋樹的判定方法。由于由未知個線程執(zhí)行的