模型檢驗中的公平性問題研究.pdf

1、模型檢驗是一種重要的自動化驗證技術(shù)，在保障軟件高可信性過程中發(fā)揮著巨大作用。近年來分布式系統(tǒng)的發(fā)展表明，模型檢驗中的公平性問題已經(jīng)引起了諸多關(guān)注。如果不考慮公平性，模型檢驗常常會產(chǎn)生一些不現(xiàn)實的回路，比如某些進(jìn)程或事件被調(diào)度器無限次地忽略，或者某些處理器永遠(yuǎn)比另外的處理器更快，而據(jù)此產(chǎn)生的反例并不是用戶真正要找的系統(tǒng)缺陷。此外，隨著模型檢驗的研究重點轉(zhuǎn)向?qū)崟r系統(tǒng)，學(xué)術(shù)界開始關(guān)注一類特殊的公平性問題，即實時系統(tǒng)中的空性檢測，該問題會對系統(tǒng)

2、的安全性驗證和活性驗證等結(jié)果產(chǎn)生消極影響，從而降低模型檢驗的正確性。本文圍繞模型檢驗中的公平性問題展開討論，重點研究了支持公平性驗證的模型檢驗算法，實時系統(tǒng)中的空性檢測算法，以及相關(guān)驗證工具的開發(fā)等子問題。論文的主要工作及貢獻(xiàn)如下:
　　1.總結(jié)了學(xué)術(shù)界存在的多種公平性定義，并將其和模型檢驗技術(shù)相結(jié)合，把支持公平性的模型檢驗問題轉(zhuǎn)化為在Bichi自動機(jī)中，查找一個可接受(acceptable)的并且同時滿足公平性約束的無窮運(yùn)行。在

3、此基礎(chǔ)上，擴(kuò)展Tarjan的SCC算法來解決回路查找問題，并提出了一個支持公平性驗證的模型檢驗算法和框架。該算法能根據(jù)不同的公平性條件，產(chǎn)生相應(yīng)的輸出。實驗表明該算法非常有效且性能良好。
　　2.模型檢驗方法的成功在很大程度上得益于驗證工具的支持，而現(xiàn)有的模型檢驗工具對公平性問題的支持很不充分。因此，本文在模型驗證工具PAT框架中開發(fā)了專門的公平性驗證的模塊，支持多類公平性約束，包括進(jìn)程層面的強(qiáng)/弱公平，事件層面的強(qiáng)/弱公平以及全

4、局強(qiáng)公平性等。該工具能以on-the-fly的方式對線性時序邏輯性質(zhì)進(jìn)行驗證。通過對兩組實驗（人口協(xié)議模型和基準(zhǔn)模型）的比較發(fā)現(xiàn)，PAT工具中的公平性算法在和SPIN的對比中占據(jù)很大的優(yōu)勢。
　　3.時間自動機(jī)是一種對實時系統(tǒng)進(jìn)行形式化建模和驗證的重要技術(shù)，本文為解決時間自動機(jī)中的空性檢測問題，定義了一類特殊的時間自動機(jī)CUB-TA，提出了基于CUB-TA的空性檢測算法，該算法不需要在時鐘帶圖中增加新的狀態(tài)或時鐘，所以能極大提高空

5、性檢測的效率。同時，還提出了一種將任意時間自動機(jī)轉(zhuǎn)化成CUB-TA的算法，并從理論上證明了其正確性。實驗結(jié)果表明，CUB-TA在基準(zhǔn)模型中較為普遍，因此該方法非常具有實用性。
　　4.如何把主流空性檢測算法放到一個實用和公平的環(huán)境中進(jìn)行對比分析，學(xué)術(shù)界目前還缺乏相關(guān)工作。本文開發(fā)了一個集成多種算法的模型檢驗工具TA@PAT，該工具中設(shè)計的啟發(fā)式規(guī)則能根據(jù)不同的輸入模型，自動選擇最優(yōu)算法進(jìn)行計算。據(jù)我們所知，TA@PAT是目前唯一能

6、直接支持基于空性檢測的LTL性質(zhì)驗證的工具。此外，通過對多個基準(zhǔn)模型進(jìn)行實驗，我們完成了一次系統(tǒng)而全面的空性檢測算法的評估，并給出了相關(guān)的結(jié)論和分析。
　　5.多層次的實時系統(tǒng)不能直接用時間自動機(jī)建模，為此學(xué)術(shù)界提出了一種新的建模語言——STCSP(Stateful Timed CSP)。為解決STCSP模型中的空性檢測問題，本文提出了一種時鐘對稱化簡方法，減小了時鐘帶圖的大小，從而極大地改進(jìn)了以往的空性檢測算法的效率。此外，還將