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

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

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

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



本文編號：4003206