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

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

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

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

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

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

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