打結(jié)不變的命題投影時邏輯與模型檢測.pdf

1、本文提出了打結(jié)不變的命題投影時序邏輯,介紹了基于該邏輯的模型檢測方法,并采用該方法驗證了無條件安全通信協(xié)議。命題投影時序邏輯(PPTL)可表達(dá)所有ω-正則式其表達(dá)能力強(qiáng)于其他線性命題時序邏輯(如PTLL),此外作為性質(zhì)描述語言,其中的projection和chop算子使得性質(zhì)定義更為靈活,因此PPTL適用于有窮狀態(tài)并發(fā)系統(tǒng)的描述和驗證?；赑PTL的模型檢測方法近年來被提出,然而其作為一種形式化驗證方法同樣要面臨狀態(tài)爆炸問題。為此,本文

2、定義了PPTL的打結(jié)不變子邏輯(記作PPTLst),證明了PPTLst可表達(dá)所有PPTL可表達(dá)的打結(jié)不變性質(zhì)。由于PPTLst定義的性質(zhì)對系統(tǒng)中打結(jié)等價的行為不做區(qū)別,所以在偏序規(guī)約驗證中,針對打結(jié)等價類只需驗證其中的一個行為而不必驗證等價類中的所有行為。因此支持PPTLst的偏序歸約技術(shù)可避免遍歷整個系統(tǒng)狀態(tài)空間?；谠撍枷氡疚膶崿F(xiàn)了支持基于PPTLst偏序規(guī)約的模型檢測器。
　　 此外,PPTLst還可作為性質(zhì)描述語言用于組

3、合驗證。其包含的projection和chop算子允許將性質(zhì)定義在系統(tǒng)路徑中受關(guān)注的狀態(tài)上,并且由這些狀態(tài)構(gòu)成的抽象路徑與原路徑打結(jié)等價。因為PPTLst定義的性質(zhì)不區(qū)分打結(jié)等價路徑,所以該抽象操作對驗證不構(gòu)成影響。由此在自下而上的組合驗證中,每層的模塊可根據(jù)其性質(zhì)先進(jìn)行抽象再向上組合。經(jīng)過逐層抽象,約減掉了與性質(zhì)無關(guān)的狀態(tài),從而可緩解狀態(tài)爆炸問題。
　　 除了以上技術(shù)外,性質(zhì)公式的簡化也可減少驗證所需遍歷的狀態(tài)個數(shù)從而提高驗證

4、效率。為了找出影響PPTLst空間復(fù)雜度的因素,本文研究了PPTLst的空間復(fù)雜度上界。為此,定義了完全正則圖(CNG),給出了PPTLst公式向CNG轉(zhuǎn)換的算法?；贑NG證明了PPTLst空間復(fù)雜度上界屬于非初等,從該證明可知PPTLst的空間復(fù)雜度由其'chop(或proliection)的非'嵌套的深度和原子命題個數(shù)兩個因素決定。因此,驗證中應(yīng)盡可能選擇'chop(或projection)的非'-嵌套較低和原子命題個數(shù)較少的公式

5、來描述性質(zhì),從達(dá)到簡化性質(zhì)公式的目的。
　　 本文將上述PPTLst模型檢測技術(shù)用于驗證Russian Cards協(xié)議以分析無條件通信的安全性。為此,首先擴(kuò)展了原始Russian Cards問題并根據(jù)該擴(kuò)展方法提出了RussianCards協(xié)議,給出了該協(xié)議的安全通信條件以及構(gòu)造安全通信序列的算法。然后,利用PPTLst組合驗證方法分析協(xié)議模型的安全性,在組合過程中,每個模塊的驗證又基于PPTLst偏序規(guī)約技術(shù)。實驗表明PPTL