隨著多核處理器和并發(fā)技術(shù)的快速發(fā)展,并發(fā)多線程程序設(shè)計成為了軟件開發(fā)的主流模式,并發(fā)系統(tǒng)被逐漸應(yīng)用于多個領(lǐng)域,為人們的生活提供了諸多便利。然而,并發(fā)系統(tǒng)的結(jié)構(gòu)一般比較復(fù)雜,且存在多個線程相互交錯執(zhí)行的情況,傳統(tǒng)的模擬和測試方法難以發(fā)現(xiàn)系統(tǒng)中的微小錯誤。通常采用模型檢測驗證并發(fā)系統(tǒng)的正確性,但并發(fā)系統(tǒng)的狀態(tài)空間隨著并發(fā)量的增加呈指數(shù)級增長,嚴重制約了模型檢測的驗證效率。謂詞抽象技術(shù)能夠有效地緩解狀態(tài)空間爆炸問題,對源程序?qū)嵤┲^詞抽象可以產(chǎn)生布爾程序,布爾程序作為程序驗證的簡單模型,在一定程度上優(yōu)化了狀態(tài)空間,提高了模型檢測的驗證效率。本文以無界線程的并發(fā)布爾程序為研究對象,分析程序中違背斷言的狀態(tài)是否可達,具體工作內(nèi)容如下:（1）研究了后向搜索算法的基本流程,分析了算法的搜索策略和最小覆蓋前驅(qū)的計算方法,并結(jié)合并發(fā)布爾程序的特點,提出一種深度優(yōu)先的后向搜索算法,對最小覆蓋前驅(qū)的計算方法進行優(yōu)化,提高了并發(fā)布爾程序可達性分析的效率。（2）研究了并發(fā)布爾程序的線程遷移系統(tǒng),在改進的算法基礎(chǔ)上,結(jié)合計數(shù)器抽象技術(shù)和summarization方法,提出了一種基于線程遷移系統(tǒng)的可達性分析模型。采用... 

【文章來源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

【文章頁數(shù)】：75 頁

【學(xué)位級別】：碩士

【文章目錄】：
摘要
ABSTRACT
符號對照表
縮略語對照表
第一章 緒論
    1.1 研究背景及意義
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 研究內(nèi)容及論文章節(jié)安排
        1.3.1 主要研究內(nèi)容
        1.3.2 章節(jié)安排
第二章 相關(guān)基礎(chǔ)理論
    2.1 模型檢測
    2.2 抽象技術(shù)
        2.2.1 謂詞抽象技術(shù)
        2.2.2 其他抽象技術(shù)
        2.2.3 基于抽象的模型檢測工具
    2.3 布爾程序
        2.3.1 順序布爾程序
        2.3.2 并發(fā)布爾程序
        2.3.3 并發(fā)布爾程序的遷移系統(tǒng)
    2.4 良擬序遷移系統(tǒng)
        2.4.1 擬序
        2.4.2 良擬序遷移系統(tǒng)
    2.5 可滿足性問題(SAT)
    2.6 本章小結(jié)
第三章 基于后向搜索算法的并發(fā)布爾程序可達性分析
    3.1 并發(fā)布爾程序的可達性問題
    3.2 后向搜索算法
    3.3 并發(fā)布爾程序的可達性分析
        3.3.1 最小覆蓋前驅(qū)
        3.3.2 可達性分析
    3.4 一種改進的BWS算法—DBWS
        3.4.1 BWS算法分析
        3.4.2 DBWS算法
        3.4.3 DBWS的擴展前驅(qū)
    3.5 本章小結(jié)
第四章 基于線程遷移系統(tǒng)的并發(fā)布爾程序可達性分析
    4.1 線程遷移系統(tǒng)
    4.2 基于線程遷移系統(tǒng)的可達性分析模型
    4.3 核心模塊的設(shè)計與實現(xiàn)
        4.3.1 擴展遷移模塊
        4.3.2 公式求解模塊
        4.3.3 擴展算法模塊
    4.4 本章小結(jié)
第五章 實驗結(jié)果分析
    5.1 實驗環(huán)境及測試集
    5.2 實驗結(jié)果分析
    5.3 本章小結(jié)
第六章 總結(jié)與展望
    6.1 工作總結(jié)
    6.2 未來展望
參考文獻
致謝
作者簡介


【參考文獻】：
期刊論文
[1]面向程序驗證的并行程序狀態(tài)空間態(tài)約簡技術(shù)綜述[J]. 逄龍,蘇小紅,馬培軍,趙玲玲.  智能計算機與應(yīng)用. 2015(01)
[2]SMT求解器理論組合技術(shù)研究[J]. 李婧,劉萬偉.  計算機工程與科學(xué). 2011(10)



本文編號：3411242