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

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

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

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