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

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

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

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

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

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

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