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

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

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

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