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

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

【學位級別】：碩士

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


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



本文編號：3729111