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

1、隨著計(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)中廣泛存在，面對(duì)日趨復(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)證方法通過符號(hào)描述帶參協(xié)議的系統(tǒng)行為及

2、其性質(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ù)，模型檢測(cè)技術(shù)在帶參協(xié)議規(guī)模較大的情況下會(huì)出現(xiàn)狀態(tài)空間爆炸的問題，這些都成為了限制帶參協(xié)議形式化驗(yàn)證有效性的重要因素。
　　本論文對(duì)現(xiàn)有的帶參協(xié)議的形式化驗(yàn)證方法進(jìn)行了分類整理和深入分析，主

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

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