弱公平條件下模型檢驗(yàn)狀態(tài)空間的對稱化簡.pdf

1、形式化驗(yàn)證已經(jīng)成為對系統(tǒng)設(shè)計(jì)和協(xié)議設(shè)計(jì)進(jìn)行確認(rèn)的重要手段,其方法分為兩類<'[42]>,一類是以邏輯推理為基礎(chǔ),另一類則以窮盡搜索為基礎(chǔ),窮盡搜索方法統(tǒng)稱為模型檢驗(yàn).邏輯推理的不足之處在于推理的難度.對于稍微復(fù)雜的系統(tǒng),自動化的推理就難以勝任.模型檢驗(yàn)的好處在于它有全自動化的檢驗(yàn)過程,并且如果一個(gè)性質(zhì)不滿足,它能給出這個(gè)性質(zhì)不滿足的理由,可據(jù)此對系統(tǒng)設(shè)計(jì)進(jìn)行改進(jìn).狀態(tài)爆炸[6]是模型檢驗(yàn)中的一個(gè)重要難題.實(shí)際系統(tǒng)中的狀態(tài)數(shù)目可能很大,以

2、至無法在有限的時(shí)間和內(nèi)存空間下進(jìn)行完整的檢驗(yàn).對稱歸約是處理狀態(tài)爆炸問題的有效技術(shù)之一.但是在實(shí)際系統(tǒng)驗(yàn)證時(shí),如果是處于公平條件下,已有的對稱歸約算法很難有有效的作用.而在實(shí)際應(yīng)用中,公平性是驗(yàn)證一些性質(zhì)的先決條件.該文給出了一個(gè)模型檢驗(yàn)的算法,在公平條件下利用對稱歸約化簡狀態(tài)空間,以改善狀態(tài)爆炸問題.這個(gè)算法基于嵌套深度優(yōu)先搜索(NDFS)算法.它假定要檢驗(yàn)的性質(zhì)用Buchi自動機(jī)<'[19]>給定,因此,檢驗(yàn)系統(tǒng)是否支持某個(gè)給定性質(zhì)

3、的問題,就歸結(jié)為在圖中尋找接受回路的問題<'[7,6]>.該文首先敘述并分析了標(biāo)準(zhǔn)的NDFS算法<'[7,17]>和帶對稱歸約的NDFS算法<'[3]>;然后通過對模型檢驗(yàn)器Spin中的弱公平性算法(由Holzmann實(shí)現(xiàn))進(jìn)行擴(kuò)展,提出了一個(gè)在弱公平條件下、未使用對稱歸約的、基于嵌套深度優(yōu)先搜(NDFS)的模型檢驗(yàn)策略,最后在此基礎(chǔ)上提出基于NDFS的融合弱公平性和對稱歸約的算法.相對于基于尋找最大強(qiáng)連通分支(MSCC)的類似算法<'

4、[11,14]>,該算法具有基于NDFS的優(yōu)勢,每個(gè)狀態(tài)的空間開銷也要少,而且,雖然與它們有相同的最壞時(shí)間復(fù)雜度O(N·| h(T)|),但是在檢測到性質(zhì)的一個(gè)反例時(shí),該算法需要遍歷的狀態(tài)要少得多,因此具有更好的時(shí)間和空間復(fù)雜性,同時(shí)也兼容于近似驗(yàn)證技術(shù).該文還把這個(gè)算法的原型運(yùn)用在通用的模型檢驗(yàn)器Spin之上,對Peterson互斥協(xié)議等例子的進(jìn)行驗(yàn)證實(shí)驗(yàn).實(shí)驗(yàn)的結(jié)果顯示,該文的算法使對稱歸約在弱公平條件下的化簡效果接近于它不在弱公平