PPTL的偏序模型檢測器的實現(xiàn)與驗證實例.pdf

1、隨著計算機技術的發(fā)展，軟硬件的正確性和可靠性已經(jīng)成為使用方關注的一項重要指標，特別是在航空航天、軍工控制系統(tǒng)中，這一點尤為明顯。模型檢測作為一種形式化驗證技術，受到各個相關領域的青睞。模型檢測的基本思想是對給定的系統(tǒng)進行建模，用時序邏輯公式表示待驗證的系統(tǒng)性質，然后用驗證器驗證該系統(tǒng)模型是否滿足給定的性質，如果不滿足給定的性質，則給出反例路徑。模型檢測雖然有著自動化驗證等優(yōu)點，但是也受制于狀態(tài)空間爆炸問題。為了緩解模型檢測過程中出現(xiàn)的狀

2、態(tài)空間爆炸問題，目前提出了很多有效的方法，如基于偏序歸約技術的偏序模型檢測等。偏序模型檢測器SPIN是由貝爾實驗室開發(fā)的開源軟件，它多用來檢測分布式軟件模型的正確性，并且它能以一種嚴格且自動化的形式進行驗證。SPIN使用Promela語言對系統(tǒng)進行建模，用LTL公式描述系統(tǒng)模型的性質，然后將該性質的非轉換成對應的Büchi自動機，最后由驗證器自動執(zhí)行驗證過程，得出結果。但是LTL的表達能力不是完全正則的，有些性質并不能用LTL公式表示出

3、來，因此需要用一種表達能力更強的時序邏輯來描述系統(tǒng)的性質。PPTL具有完全正則的表達能力，并且PPTL的可判定性也已經(jīng)得到了證明，因此本文實現(xiàn)了基于SPIN的PPTL偏序模型檢測器，并給出了該偏序模型檢測器的驗證實例。
　　本文首先研究了PPTL公式到Büchi自動機的轉換算法包括PPTL公式到帶標記的范式圖的轉換、帶標記的范式圖到廣義Büchi自動機的轉換和廣義Büchi自動機到Büchi自動機的轉換。然后在SPIN的基礎上增加

4、了PPTL公式到NeverClaim形式的轉換過程，實現(xiàn)了PPTL的偏序模型檢測器。給出了PPTL公式到NeverClaim形式的轉換過程的設計類圖、主要函數(shù)以及各個模塊的程序流程圖，并用兩個PPTL公式轉換實例展示了該轉換過程生成的帶標記的范式圖、Büchi自動機和NeverClaim形式。最后給出了基于密碼協(xié)議的KDC協(xié)議的驗證實例，用Promela語言對KDC協(xié)議進行建模，用PPTL公式描述該協(xié)議的性質，并利用該模型檢測器檢測出K