模型檢驗(yàn)中的公平性問題研究.pdf

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

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

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

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

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

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