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

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

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

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

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

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