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

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

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

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

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