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

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

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

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

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

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