[發明專利]一種面向限界檢測技術的系統模型構造方法

無效

• 申請號: 201310034737.0
• 申請日: 2013-01-29
• 公開（公告）號: CN103049277A
• 公開（公告）日: 2013-04-17
• 發明（設計）人: 周從華
• 申請（專利權）人: 江蘇大學
• 主分類號: G06F9/44
• 分類號: G06F9/44
• 代理公司: 南京知識律師事務所 32207
• 代理人: 盧亞麗

技術領域

本發明屬于隨機系統性能分析技術領域，涉及以概率模型檢測工具PRISM為分析工具，面向以局部空間為搜索對象的限界檢測技術的隨機系統建模方法。?

背景技術

模型檢測是一種自動化程度非常高的有限狀態系統驗證技術，目前已經在計算機硬件、通信協議、安全協議的驗證方面獲得了較大的成功。傳統的模型檢測技術關注的是系統行為的絕對正確性，如系統不能進入死鎖狀態。然而在實際的系統中存在很多隨機現象，例如不可靠信道上的消息丟失，對這一類現象往往關心某種概率度量，如消息傳送失敗的概率不高于1%等等。傳統模型檢測中使用的邏輯系統，如計算樹和線性時態邏輯，無法刻畫這類屬性，因此研究人員在計算樹和線性時態邏輯的基礎上引入了概率算子，得到了概率計算樹邏輯PCTL等邏輯系統，并提出了馬爾科夫鏈，隨機Petri網等不同隨機模型上的概率模型檢測方法。?

PRISM是由牛津大學的Marta?Kwiatkowska教授主導開發，一款面向學術界可免費使用的概率模型檢測工具，主要用來對隨機系統的行為進行建模與分析。目前PRISM已經成功應用于通信與多媒體協議，隨機分布式算法，安全協議，以及生物系統等領域的分析當中。使用PRISM進行性能與可靠性自動化分析的過程可以概括為：1)利用PRISM自定義的系統建模語言為隨機系統建立模型；2)利用概率邏輯PCTL或者CSL描述待分析的屬性；3)調用全局模型檢測算法自動完成分析過程。?

與傳統模型檢測一樣，狀態空間爆炸問題是PRISM進一步走向實用化的主要瓶頸，這里狀態空間爆炸是指系統狀態空間的大小隨著進程數量的增加呈指數級增長。為緩解該問題，傳統模型檢測中的空間約簡技術，如謂詞抽象、偏序歸約、對稱歸約、組合推理等均可被應用到PRISM上。目前PRISM只支持精確模型上的計算，因此實施這些約簡技術需要修改PRISM的源代碼，增加相應的處理模塊。源代碼的修改使得這些約簡技術在實施上可操作性較差，工作量巨大。?

限界檢測是新近出現的一種空間約簡技術，其基本思想是在有限的局部空間中逐步搜索屬性成立的證據或者失效的反例，從而達到約簡狀態空間的目的。限界檢測的實現過程主要包括兩個部分：1)在局部空間上定義概率邏輯的限界語義；2）設計局部空間上限界語義的可滿足性判定算法。只遍歷分析屬性所需的局部空間是限界檢測能夠有效克服狀態空間爆炸的主要原因。PRISM目前具有一定的逐步計算局部空間的功能，只支持隨機系統模型上無界語義的滿足性判定算法，但是由于對狀態轉換關系采取了近似表示，如在可達深度為2時，利用路徑s₀→s₁→s₀替代循環結構s₀→s₁→s₀→s₁→L?L，無法直接實現限界檢測。限界檢測采用的是邏輯系統的限界語義，這與全局檢測采用的無界語義存在很大的不同。因此與謂詞抽象、偏序歸約等約簡技術一樣，在PRISM中為實現限界檢測算法必須大量修改PRISM的源代碼，并重新編譯以實現步長限制下各種概率度量的近似計算。PRISM的源程序目前包含20個文件夾，平均每個文件夾包含20個文件，要具備修改PRISM源代碼的能力必須熟悉這400個左右的文件，而且掌握近1000個函數之間的相互調用關系，因此修改PRISM源代碼是非常困難的，這使得在PRISM上執行限界檢測算法的可操作性很差，而且工作量巨大。?

發明內容

本發明的目的在于提供一種面向限界檢測技術的系統模型構造方法，以提高在PRISM上執行限界檢測技術的可操作性，降低工作量，同時保證利用限界檢測技術約簡狀態空間的效果。?

為了解決以上技術問題，本發明的采用的技術方案如下。?

一種面向限界檢測技術的系統模型構造方法，其特征在于包括以下步驟：?

步驟一，設整數k為所需構造的局部空間的深度，在建模語言的全局變量聲明處引入一個新的全局變量newv，并設置成整數型，初始值為0，即添加語句newv:[0..k]init0；?

步驟二，對語言中的每一條命令，依據符號“+”表示的概率分布進行分解，具體分解規則如下：?

原始命令：[]guard_1->prob_1:update_1+...+prob_n:update_n?

分解后的命令：?

步驟三,對每一個模塊，依據各命令中值為真的謂詞的數量以及謂詞之間組合的不同重新構造模型，進一?步具體為：?