多線程程序是計(jì)算機(jī)軟件設(shè)計(jì)的核心,如何高效驗(yàn)證多線程程序的安全性問(wèn)題已成為國(guó)內(nèi)外研究人員的主要研究?jī)?nèi)容�，F(xiàn)有研究表明:多線程程序的安全性問(wèn)題可簡(jiǎn)化為良擬序遷移系統(tǒng)(Well-Quasi-Ordered Transition System,WQOTS)的可覆蓋性問(wèn)題。針對(duì)良擬序遷移系統(tǒng)的可覆蓋性問(wèn)題,已存在大量的解決方案,它們主要是以顯示狀態(tài)搜索思想設(shè)計(jì)的。多線程程序的狀態(tài)空間隨程序的規(guī)模和線程數(shù)目的增加呈指數(shù)級(jí)增長(zhǎng),導(dǎo)致這些算法都存在低效性或不完備性的問(wèn)題。如何在驗(yàn)證過(guò)程中盡量避免狀態(tài)空間搜索或降低狀態(tài)空間的規(guī)模是提高多線程程序安全性驗(yàn)證效率的關(guān)鍵。本文主要的研究對(duì)象是被無(wú)窮個(gè)線程并發(fā)執(zhí)行的有限狀態(tài)布爾程序(Boolean Program,BP),可以通過(guò)對(duì)多線程程序進(jìn)行謂詞抽象得到。本文根據(jù)目前多線程程序驗(yàn)證方法的優(yōu)勢(shì)和不足,考慮到基于SMT求解器的符號(hào)分析方法能避免對(duì)狀態(tài)空間搜索從而加快驗(yàn)證,以及直接使用布爾程序作為抽象模型能降低狀態(tài)空間的規(guī)模,提出了一種新的多線程程序安全性驗(yàn)證方法。首先研究了基于SMT求解器的符號(hào)分析模塊,詳細(xì)分析了如何利用計(jì)數(shù)抽象從線程遷移系統(tǒng)中構(gòu)造可覆蓋性問(wèn)...

【文章頁(yè)數(shù)】：71 頁(yè)

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

【文章目錄】：
摘要
ABSTRACT
符號(hào)對(duì)照表
縮略語(yǔ)對(duì)照表
第一章 緒論
    1.1 研究背景和意義
    1.2 國(guó)內(nèi)外研究進(jìn)展
    1.3 研究?jī)?nèi)容及論文章節(jié)安排
        1.3.1 主要研究?jī)?nèi)容
        1.3.2 組織結(jié)構(gòu)
第二章 相關(guān)基礎(chǔ)理論
    2.1 模型檢測(cè)
    2.2 抽象技術(shù)
        2.2.1 謂詞抽象技術(shù)
        2.2.2 常見(jiàn)的謂詞抽象工具
    2.3 布爾程序
        2.3.1 順序布爾程序
        2.3.2 并發(fā)布爾程序和無(wú)限狀態(tài)遷移系統(tǒng)
    2.4 良擬序遷移系統(tǒng)
        2.4.1 Petri網(wǎng)系統(tǒng)
        2.4.2 線程遷移系統(tǒng)
    2.5 可達(dá)性問(wèn)題和可覆蓋性問(wèn)題的關(guān)聯(lián)
    2.6 本章小結(jié)
第三章 基于SMT和BP的多線程程序的可覆蓋性分析
    3.1 TTS上的基于SMT求解器的可覆蓋性分析
        3.1.1 基于SMT求解器的符號(hào)分析模塊思想
        3.1.2 局部狀態(tài)約束
        3.1.3 共享狀態(tài)約束
    3.2 基于BP的KM算法模塊
        3.2.1 經(jīng)典的基于TTS的KM算法分析
        3.2.2 布爾程序上的可覆蓋性問(wèn)題
        3.2.3 布爾程序上的KM算法
    3.3 基于SMT和BP的可覆蓋性分析過(guò)程設(shè)計(jì)與實(shí)現(xiàn)
        3.3.1 工具的設(shè)計(jì)與實(shí)現(xiàn)
        3.3.2 使用改進(jìn)的KM算法的可覆蓋性分析
    3.4 本章小結(jié)
第四章 實(shí)驗(yàn)結(jié)果分析
    4.1 實(shí)驗(yàn)環(huán)境及測(cè)試集
    4.2 實(shí)驗(yàn)結(jié)果分析
    4.3 本章小結(jié)
第五章 總結(jié)與展望
    5.1 工作總結(jié)
    5.2 未來(lái)展望
參考文獻(xiàn)
致謝
作者簡(jiǎn)介



本文編號(hào)：4003206