復(fù)雜隨機(jī)系統(tǒng)模型檢測方法研究.pdf

1、隨著信息技術(shù)的快速發(fā)展，各種軟、硬件系統(tǒng)在社會生活中占據(jù)著越來越重要的位置，系統(tǒng)的安全性與可靠性因此變得越來越重要。功能正確性與性能可滿足性日益成為學(xué)術(shù)界關(guān)注的熱點問題，采用有效的手段來驗證系統(tǒng)的功能及性能特征是否滿足要求已成為日益重要的研究課題。
　　形式化方法被認(rèn)為是系統(tǒng)性能可信評估方面可行、有效的方法之一。其中模型檢測技術(shù)因其自動化程度高且具有嚴(yán)格的數(shù)學(xué)基礎(chǔ)等優(yōu)點而被廣泛應(yīng)用，研究熱點包括硬件驗證、協(xié)議分析等領(lǐng)域并逐漸轉(zhuǎn)移到

2、軟件驗證領(lǐng)域，關(guān)注的重點也由對系統(tǒng)行為的定性分析轉(zhuǎn)向定性分析與定量分析相結(jié)合的復(fù)雜參數(shù)性質(zhì)驗證。
　　對于包含多種參數(shù)特征的復(fù)雜隨機(jī)系統(tǒng)，模型檢測的首要問題就是如何對系統(tǒng)進(jìn)行精確地建模并進(jìn)行性質(zhì)特征的有效刻畫，此外傳統(tǒng)模型檢測技術(shù)中出現(xiàn)的狀態(tài)空間爆炸問題以及如何采用高效的復(fù)雜隨機(jī)系統(tǒng)性質(zhì)驗證算法并對反例信息進(jìn)行有效表示與理解，亦成為影響復(fù)雜隨機(jī)系統(tǒng)模型檢測技術(shù)應(yīng)用、普及的新障礙。因此，對模型檢測理論及其在復(fù)雜隨機(jī)系統(tǒng)領(lǐng)域的應(yīng)用進(jìn)行

3、深入研究具有較高的理論和應(yīng)用價值。
　　針對模型檢測在復(fù)雜隨機(jī)系統(tǒng)驗證中面臨的主要問題，本文開展了以下幾個方面的工作。
　　（1）對模型檢測技術(shù)中的時序邏輯及模型表示方法進(jìn)行綜合分析，提出了一種用于復(fù)雜隨機(jī)系統(tǒng)性質(zhì)描述的新型連續(xù)隨機(jī)邏輯 aCSRL，并給出對應(yīng)的系統(tǒng)模型建模表示方法，相應(yīng)的模型命名為 CTMRDP，對模型的動態(tài)行為做出嚴(yán)格的表達(dá)的同時，對比分析了aCSRL與現(xiàn)有的用于復(fù)雜隨機(jī)系統(tǒng)性質(zhì)描述的相關(guān)時序邏輯，證明了

4、其表達(dá)能力嚴(yán)格強(qiáng)于相關(guān)的其它連續(xù)邏輯。
　?。?）提出了用于復(fù)雜隨機(jī)系統(tǒng)模型CTMRDP的aCSRL性質(zhì)驗證方法。通過特征消去、強(qiáng)連通子圖構(gòu)造等步驟，采用類似CSL模型檢測的方法完成了aCSRL穩(wěn)態(tài)概率狀態(tài)公式的求解并進(jìn)行實例分析。對于 aCSRL瞬時概率狀態(tài)公式，通過對其所包含的路徑公式的結(jié)構(gòu)分析，基于自動機(jī)理論給出了aCSRL路徑公式的形式化表示，借鑒傳統(tǒng)的LTL模型檢測方法，給出了路徑公式自動機(jī)與系統(tǒng)模型的同步自動機(jī)模型的定

5、義，提出了基于同步自動機(jī)模型下的時間、回報特征約束下的性質(zhì)定量驗證方法，并進(jìn)行了算法描述，通過實例分析證明了復(fù)雜隨機(jī)系統(tǒng)模型 aCSRL時序邏輯性質(zhì)驗證的可行性與有效性。
　?。?）針對離散概率回報模型，提出了多重直到約束路徑公式及條件概率狀態(tài)公式的邏輯語義，通過構(gòu)造多重直到公式及多重直到合取公式自動機(jī)，基于同步自動機(jī)模型對相應(yīng)的性質(zhì)驗證方法并進(jìn)行了實例分析，同時基于離散概率回報模型轉(zhuǎn)化得到的帶權(quán)有向圖，采用迭代求解方式提出了多重

6、直到約束路徑公式及條件概率狀態(tài)公式定量驗證求解算法，通過實例構(gòu)造分析證明了算法的有效性，同時提出了離散概率回報模型性質(zhì)反例的正則表達(dá)式壓縮表示方法以及反例自動機(jī)模型表示方法。
　?。?）針對復(fù)雜隨機(jī)系統(tǒng)模型性質(zhì)驗證的狀態(tài)空間爆炸問題，提出一種應(yīng)用于馬爾可夫回報模型的狀態(tài)空間約減的方法。該方法首先利用符號編碼方式對模型進(jìn)行二元決策圖表示，而后利用對稱約減技術(shù)，結(jié)合了互模擬理論通過分析原始模型中的等價類關(guān)系，借助等價類唯一表示函數(shù)，基