帶參協(xié)議形式化驗證的研究.pdf

1、隨著計算機技術(shù)、網(wǎng)絡(luò)技術(shù)以及電子信息技術(shù)在各行各業(yè)的日益發(fā)展，多處理器體系以及多核架構(gòu)在計算機系統(tǒng)結(jié)構(gòu)中應(yīng)用得越來越頻繁，其正確性、可靠性等問題也越來越突出。帶參協(xié)議在計算機系統(tǒng)多處理器體系的核心結(jié)構(gòu)中廣泛存在，面對日趨復(fù)雜的設(shè)計，帶參協(xié)議正確性的驗證越來越成為設(shè)計流程中的關(guān)鍵，細微的錯誤可能引發(fā)嚴重的后果。因此，帶參協(xié)議設(shè)計正確性的驗證問題成為了學(xué)術(shù)界和工業(yè)界研究的熱點和重點。
　　形式化驗證方法通過符號描述帶參協(xié)議的系統(tǒng)行為及

2、其性質(zhì)，基于各種數(shù)學(xué)邏輯推理算法進行驗證，驗證覆蓋率高，且具有完備性，目前已經(jīng)成為帶參協(xié)議驗證的重要方法。在帶參協(xié)議形式化驗證領(lǐng)域，雖然已經(jīng)存在多種形式化驗證方法，但是每種方法都存在一定的缺點，例如定理證明技術(shù)的自動化程度不高，需要人為主動干預(yù)，模型檢測技術(shù)在帶參協(xié)議規(guī)模較大的情況下會出現(xiàn)狀態(tài)空間爆炸的問題，這些都成為了限制帶參協(xié)議形式化驗證有效性的重要因素。
　　本論文對現(xiàn)有的帶參協(xié)議的形式化驗證方法進行了分類整理和深入分析，主

3、要從提高定理證明技術(shù)的自動化程度和緩解模型檢測技術(shù)狀態(tài)空間的爆炸現(xiàn)象兩個角度入手，提出了兩種驗證方法，并且在MESI、MutualEx、GERMAN、FLASH等典型的帶參協(xié)議上驗證了它們的有效性，主要的研究成果如下:
　　(1)提出了一種基于歸納不變式和流分析結(jié)合的驗證方法。該方法分析了帶參協(xié)議的不變式和遷移規(guī)則實例之間存在的因果關(guān)系，通過歸納不變查找算法自動查找?guī)f(xié)議的歸納不變式，為使用定理證明工具構(gòu)造定理證明腳本提供了便利

4、。除此之外，引入了流分析的概念，在驗證前期對帶參協(xié)議的內(nèi)容進行了流分析，將歸納不變式和流分析結(jié)合起來進一步對帶參協(xié)議進行了驗證。本文給出了該方法的整體框架和具體實現(xiàn)，并在多個典型帶參協(xié)議中驗證了該方法的有效性。
　　(2)提出了一種基于CVC4的謂詞抽象的驗證方法。該方法將謂詞抽象的思想應(yīng)用到Murphi模型檢測技術(shù)中，借助CVC4求解器求出帶參協(xié)議原有狀態(tài)對應(yīng)的抽象狀態(tài)，把系統(tǒng)性質(zhì)的驗證從原始狀態(tài)轉(zhuǎn)移到抽象狀態(tài)，在一定程度上解決