隨著計(jì)算機(jī)技術(shù)、網(wǎng)絡(luò)技術(shù)以及電子信息技術(shù)在各行各業(yè)的日益發(fā)展,多處理器體系以及多核架構(gòu)在計(jì)算機(jī)系統(tǒng)結(jié)構(gòu)中應(yīng)用得越來越頻繁,其正確性、可靠性等問題也越來越突出。帶參協(xié)議在計(jì)算機(jī)系統(tǒng)多處理器體系的核心結(jié)構(gòu)中廣泛存在,面對日趨復(fù)雜的設(shè)計(jì),帶參協(xié)議正確性的驗(yàn)證越來越成為設(shè)計(jì)流程中的關(guān)鍵,細(xì)微的錯(cuò)誤可能引發(fā)嚴(yán)重的后果。因此,帶參協(xié)議設(shè)計(jì)正確性的驗(yàn)證問題成為了學(xué)術(shù)界和工業(yè)界研究的熱點(diǎn)和重點(diǎn)。形式化驗(yàn)證方法通過符號描述帶參協(xié)議的系統(tǒng)行為及其性質(zhì),基于各種數(shù)學(xué)邏輯推理算法進(jìn)行驗(yàn)證,驗(yàn)證覆蓋率高,且具有完備性,目前已經(jīng)成為帶參協(xié)議驗(yàn)證的重要方法。在帶參協(xié)議形式化驗(yàn)證領(lǐng)域,雖然己經(jīng)存在多種形式化驗(yàn)證方法,但是每種方法都存在一定的缺點(diǎn),例如定理證明技術(shù)的自動(dòng)化程度不高,需要人為主動(dòng)干預(yù),模型檢測技術(shù)在帶參協(xié)議規(guī)模較大的情況下會(huì)出現(xiàn)狀態(tài)空間爆炸的問題,這些都成為了限制帶參協(xié)議形式化驗(yàn)證有效性的重要因素。本論文對現(xiàn)有的帶參協(xié)議的形式化驗(yàn)證方法進(jìn)行了分類整理和深入分析,主要從提高定理證明技術(shù)的自動(dòng)化程度和緩解模型檢測技術(shù)狀態(tài)空間的爆炸現(xiàn)象兩個(gè)角度入手,提出了兩種驗(yàn)證方法,并且在MESI、MutualEx、GERM... 

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

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

【文章目錄】：
致謝
摘要
ABSTRACT
1 引言
    1.1 研究背景與意義
    1.2 國內(nèi)外研究現(xiàn)狀
    1.3 論文主要研究內(nèi)容
    1.4 論文組織結(jié)構(gòu)
2 帶參協(xié)議驗(yàn)證相關(guān)理論
    2.1 帶參協(xié)議簡介
    2.2 帶參協(xié)議形式化驗(yàn)證
    2.3 帶參協(xié)議模型
        2.3.1 Murphi模型組成
        2.3.2 Murphi驗(yàn)證過程
    2.4 本章小結(jié)
3 基于歸納不變式與流分析結(jié)合的驗(yàn)證方法
    3.1 相關(guān)定義
    3.2 方法的詳細(xì)設(shè)計(jì)
        3.2.1 整體框架
        3.2.2 因果關(guān)系判定算法
        3.2.3 歸納不變式查找算法
        3.2.4 流分析
    3.3 實(shí)驗(yàn)結(jié)果
        3.3.1 典型帶參協(xié)議簡介
        3.3.2 實(shí)驗(yàn)結(jié)果展示
        3.3.3 GERMAN協(xié)議實(shí)驗(yàn)結(jié)果分析
    3.4 本章小結(jié)
4 基于CVC4的謂詞抽象的驗(yàn)證方法
    4.1 相關(guān)定義
    4.2 方法的詳細(xì)設(shè)計(jì)
        4.2.1 整體框架
        4.2.2 抽象狀態(tài)查找算法
    4.3 實(shí)驗(yàn)結(jié)果
    4.4 本章小結(jié)
5 結(jié)論
    5.1 論文總結(jié)
    5.2 論文展望
參考文獻(xiàn)
作者簡歷及攻讀碩士學(xué)位期間取得的研究成果
學(xué)位論文數(shù)據(jù)集


【參考文獻(xiàn)】：
期刊論文
[1]一種基于廣播的cache一致性協(xié)議的設(shè)計(jì)和驗(yàn)證[J]. 李俊,袁愛東,高劍剛.  計(jì)算機(jī)科學(xué)與探索. 2008(05)
[2]CMP中Cache一致性協(xié)議的驗(yàn)證[J]. 李崇民,王海,李兆麟.  電子技術(shù)應(yīng)用. 2005(12)



本文編號：3729111