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

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

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

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

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

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

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