【摘要】：多值模型檢測(cè)是解決形式化驗(yàn)證中狀態(tài)爆炸問(wèn)題的一種重要方法,三值模型檢測(cè)是多值模型檢測(cè)的基礎(chǔ),其中如何檢驗(yàn)不確定狀態(tài)的真值是一難點(diǎn)。針對(duì)不確定狀態(tài)檢驗(yàn),提出了一種模型檢測(cè)方法,首先對(duì)不完全Kripke結(jié)構(gòu)PKS進(jìn)行了擴(kuò)展,然后在擴(kuò)展后的模型上給出了檢測(cè)不確定狀態(tài)真值的方法,最后給出了基于擴(kuò)展不完全Kripke結(jié)構(gòu)的三值邏輯模型檢測(cè)算法。與已有的三值邏輯模型檢測(cè)算法相比,該算法降低了算法復(fù)雜度,完善了對(duì)于不確定或不一致信息的處理,從而增強(qiáng)了三值邏輯模型檢測(cè)的實(shí)用性。
【圖文】：

Ｆｉｇｕｒｅ１Ｐｒｏｃｅｓｓｏｆｓｔａｔｅｍｅｒｇｉｎｇ圖１狀態(tài)合并過(guò)程運(yùn)而生。本文提出一種基于三值邏輯的模型檢測(cè)方法，可作為多值模型檢測(cè)基矗在現(xiàn)有的多值邏輯模型檢測(cè)方法中，一種方法是將多值邏輯轉(zhuǎn)化為經(jīng)典邏輯進(jìn)行處理，如ＣｈｅｃｈｉｋＭ［２～５］和ＢｏｌｃＬ［６］等將已有三值問(wèn)題分解成若干經(jīng)典邏輯問(wèn)題進(jìn)行處理；而另一種方法是基于三值邏輯本身完成模型檢測(cè)，如ＬｉＹｏｎｇ－ｍｉｎｇ等［７，８］通過(guò)人為設(shè)置狀態(tài)不確定性的可接受度，采用模糊模型檢測(cè)計(jì)算出系統(tǒng)滿足性質(zhì)的可接受度。而郭建等［９］通過(guò)算法在模型檢測(cè)過(guò)程中對(duì)公式為真和未知的情況作出檢查，再由此推斷出公式為假的情況，這樣可以及早發(fā)現(xiàn)未知公式，了解哪些狀態(tài)需要信息細(xì)化，以便檢驗(yàn)未知公式的真值，但其算法中并未涉及狀態(tài)信息的細(xì)化，無(wú)法檢測(cè)未知公式的真值，三值模型檢測(cè)算法不完整。本文提出了一種三值邏輯模型檢測(cè)過(guò)程，并給出三值邏輯模型檢測(cè)算法。與已有的三值邏輯模型檢測(cè)算法相比，該算法降低了算法的復(fù)雜度，完善了對(duì)于不確定或者不一致信息的處理，從而增強(qiáng)了三值邏輯模型檢測(cè)的可應(yīng)用性。２三值邏輯模型三值邏輯模型可以在經(jīng)典邏輯模型的基礎(chǔ)上，通過(guò)對(duì)經(jīng)典邏輯模型中部分狀態(tài)進(jìn)行合并或抽取得到，從而減少系統(tǒng)狀態(tài)數(shù)量，以避免系統(tǒng)檢測(cè)中出現(xiàn)狀態(tài)爆炸。值得注意的是，在狀態(tài)遷移過(guò)程中狀態(tài)變量的數(shù)量是不變的，所以當(dāng)相鄰的一個(gè)或多個(gè)狀態(tài)進(jìn)行合并時(shí)，只需考慮狀態(tài)變量值存在不一致性的情況，即狀態(tài)變量具有多個(gè)不同的值，記此類(lèi)變量的值為Ｍ，生成三值邏輯模型。例如，圖１（１）中，由于存在搜索路徑［Ｓ０Ｓ２］ｗ、路徑［Ｓ０Ｓ１］

Ｋｌｅｅｎｅ最強(qiáng)三值邏輯命題；（３）三值系統(tǒng)模型要與原系統(tǒng)模型相一致。如圖１（２）所示，若狀態(tài)Ｓ０與Ｓ１合并，則只有Ａ不確定；若Ｓ０與Ｓ２合并，則存在Ａ、Ｂ兩個(gè)不確定變量，所以應(yīng)將Ｓ０與Ｓ１合并，其搜索路徑為［（Ｓ０，１）ｗＳ２］ｗ，較圖１（１）明顯減少。三值模型檢驗(yàn)是針對(duì)帶有不確定和不一致信息的系統(tǒng)而建立起來(lái)的一套形式驗(yàn)證理論，是經(jīng)典模型檢驗(yàn)的擴(kuò)展。下面給出了一種三值邏輯模型檢測(cè)的基本過(guò)程，如圖２所示。Ｆｉｇｕｒｅ２Ｐｒｏｃｅｓｓｏｆ３－ｖａｌｕｅｄｍｏｄｅｌｃｈｅｃｋｉｎｇｖａｌｉｄａｔｉｏｎ圖２三值邏輯模型驗(yàn)證過(guò)程①經(jīng)典邏輯模型抽象為三值邏輯模型；②在系統(tǒng)模型中，除要檢測(cè)的狀態(tài)變量外，其他變量都設(shè)置為Ｍ（因不同的待驗(yàn)證系統(tǒng)性質(zhì)與不同的系統(tǒng)變量相關(guān)，，而系統(tǒng)模型卻與所有系統(tǒng)變量相關(guān)，這樣做的目的是為減少驗(yàn)證過(guò)程中不必要的計(jì)算），利用多值模型檢測(cè)器檢測(cè)狀態(tài)是否滿足系統(tǒng)所需的性質(zhì)Ｐ；若模型檢測(cè)器返回Ｔ或Ｆ，檢測(cè)結(jié)束；③如果檢測(cè)器返回Ｍ，返回原三值邏輯模型，增加信息，重新設(shè)置變量，再進(jìn)行檢測(cè)；④三值邏輯模型的所有確定信息都被檢測(cè)后，檢測(cè)器仍返回Ｍ，則返回到經(jīng)典邏輯模型；⑤多值模型檢測(cè)器對(duì)經(jīng)典模型進(jìn)行驗(yàn)證，驗(yàn)證未知性質(zhì)的真值，檢測(cè)結(jié)束。３三值邏輯模型檢測(cè)實(shí)現(xiàn)模型檢測(cè)是在描述系統(tǒng)的狀態(tài)遷移系統(tǒng)Ｋ上驗(yàn)證時(shí)序邏輯公式ｐ描述的系統(tǒng)性質(zhì)是否可滿足的一個(gè)過(guò)程。經(jīng)典模型檢測(cè)使用Ｋｒｉｐｋｅ結(jié)構(gòu)來(lái)對(duì)系統(tǒng)建模，而三值模型檢驗(yàn)通常使用不完全Ｋｒｉｐ－ｋｅ結(jié)構(gòu)對(duì)系統(tǒng)建模。本文對(duì)原有
【作者單位】： 陜西師范大學(xué)計(jì)算機(jī)科學(xué)學(xué)院;
【基金】：國(guó)家自然科學(xué)基金資助項(xiàng)目(61003061;11271237)
【分類(lèi)號(hào)】：TP306

【參考文獻(xiàn)】

相關(guān)期刊論文 前1條

1 郭建;韓俊剛;;基于不完全Kripke結(jié)構(gòu)三值邏輯的模型檢驗(yàn)[J];計(jì)算機(jī)科學(xué);2006年03期

【共引文獻(xiàn)】

相關(guān)期刊論文 前3條

1 林杰;余建坤;;基于Kripke結(jié)構(gòu)的程序正確性證明[J];計(jì)算機(jī)應(yīng)用;2011年05期

2 余亞剛;邱征;魏雪菲;;一種可擴(kuò)展的C代碼靜態(tài)分析方法研究[J];科技風(fēng);2012年14期

3 韓樹(shù)森;戴航;;模型檢驗(yàn)下蠕蟲(chóng)病毒檢測(cè)器的設(shè)計(jì)與實(shí)現(xiàn)[J];現(xiàn)代電子技術(shù);2012年03期

【相似文獻(xiàn)】

相關(guān)期刊論文 前7條

1 張軼,林惠民;帶復(fù)雜數(shù)據(jù)結(jié)構(gòu)的模型檢測(cè)工具[J];計(jì)算機(jī)研究與發(fā)展;2004年11期

2 吳立軍;駱翔宇;陳清亮;;基于動(dòng)態(tài)內(nèi)存和狀態(tài)管理的模型檢測(cè)新方法[J];計(jì)算機(jī)科學(xué);2011年11期

3 肖美華;熊昊;;模型檢測(cè)中反例最小化分析[J];南昌大學(xué)學(xué)報(bào)(工科版);2008年04期

4 勾利杰;李真;王從銀;莊雷;;一種模型檢測(cè)精確加速的判斷方法[J];中原工學(xué)院學(xué)報(bào);2014年04期

5 潘志鶴,李祥;ANSI-C語(yǔ)言的有界模型檢測(cè)及其在硬件驗(yàn)證中的應(yīng)用[J];電腦與信息技術(shù);2005年04期

6 朱明,邊計(jì)年,吳為民;基于CDFG和OVL的系統(tǒng)驗(yàn)證性質(zhì)分類(lèi)[J];計(jì)算機(jī)工程;2005年10期

7 ;[J];;年期

相關(guān)博士學(xué)位論文 前2條

1 林榮德;移動(dòng)界程演算及模型檢測(cè)應(yīng)用的關(guān)鍵問(wèn)題研究[D];華南理工大學(xué);2010年

2 陳冬火;超協(xié)調(diào)時(shí)序邏輯及其模型檢測(cè)方法[D];中國(guó)科學(xué)院研究生院（成都計(jì)算機(jī)應(yīng)用研究所）;2006年

相關(guān)碩士學(xué)位論文 前6條

1 汪永虎;基于內(nèi)存和狀態(tài)管理的模型檢測(cè)方法[D];電子科技大學(xué);2012年

2 何青;模型檢測(cè)時(shí)態(tài)知識(shí)邏輯及其應(yīng)用[D];中山大學(xué);2006年

3 李召妮;基于自動(dòng)機(jī)和可能性Kripke結(jié)構(gòu)的模型檢測(cè)理論應(yīng)用研究[D];陜西師范大學(xué);2014年

4 安鑫;面向一類(lèi)基于輪數(shù)的分布式算法的狀態(tài)空間分析與模型檢測(cè)[D];山東大學(xué);2010年

5 魏小勇;符號(hào)模型檢測(cè)的研究[D];西安理工大學(xué);2008年

6 狄楊思;形式規(guī)范的自動(dòng)驗(yàn)證算法的研究[D];南京航空航天大學(xué);2012年

本文編號(hào)：2537369