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

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

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

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

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