一種面向限界檢測技術的系統模型構造方法
2023-06-03 08:41:31 1
專利名稱：一種面向限界檢測技術的系統模型構造方法
技術領域：
本發明屬於隨機系統性能分析技術領域，涉及以概率模型檢測工具PRISM為分析工具，面向以局部空間為搜索對象的限界檢測技術的隨機系統建模方法。
背景技術：
模型檢測是一種自動化程度非常高的有限狀態系統驗證技術，目前已經在計算機硬體、通信協議、安全協議的驗證方面獲得了較大的成功。傳統的模型檢測技術關注的是系統行為的絕對正確性，如系統不能進入死鎖狀態。然而在實際的系統中存在很多隨機現象，例如不可靠信道上的消息丟失，對這一類現象往往關心某種概率度量，如消息傳送失敗的概率不高於1%等等。傳統模型檢測中使用的邏輯系統，如計算樹和線性時態邏輯，無法刻畫這類屬性，因此研究人員在計算樹和線性時態邏輯的基礎上引入了概率算子，得到了概率計算樹邏輯PCTL等邏輯系統，並提出了馬爾科夫鏈，隨機Petri網等不同隨機模型上的概率模型檢測方法。PRISM是由牛津大學的Marta Kwiatkowska教授主導開發,一款面向學術界可免費使用的概率模型檢測工具，主要用來對隨機系統的行為進行建模與分析。目前PRISM已經成功應用於通信與多媒體協議，隨機分布式算法，安全協議，以及生物系統等領域的分析當中。使用PRISM進行性能與可靠性自動化分析的過程可以概括為1)利用PRISM自定義的系統建模語言為隨機系統建立模型；2)利用概率邏輯PCTL或者CSL描述待分析的屬性；3)調用全局模型檢測算法自動完成分析過程。與傳統模型檢測一樣，狀態空間爆炸問題是PRISM進一步走向實用化的主要瓶頸，這裡狀態空間爆炸是指系統狀態空間的大小隨著進程數量的增加呈指數級增長。為緩解該問題，傳統模型檢測中的空間約簡技術，如謂詞抽象、偏序歸約、對稱歸約、組合推理等均可被應用到PRISM上。目前PRISM只支持精確模型上的計算，因此實施這些約簡技術需要修改PRISM的原始碼，增加相應的處理模塊。原始碼的修改使得這些約簡技術在實施上可操作性較差，工作量巨大。限界檢測是新近出現的一種空間約簡技術，其基本思想是在有限的局部空間中逐步搜索屬性成立的證據或者失效的反例，從而達到約簡狀態空間的目的。限界檢測的實現過程主要包括兩個部分1)在局部空間上定義概率邏輯的限界語義；2)設計局部空間上限界語義的可滿足性判定算法。只遍歷分析屬性所需的局部空間是限界檢測能夠有效克服狀態空間爆炸的主要原因。PRISM目前具有一定的逐步計算局部空間的功能，只支持隨機系統模型上無界語義的滿足性判定算法，但是由於對狀態轉換關係採取了近似表示，如在可達深度為2時,利用路徑Stl — S1 — S0替代循環結構Stl — S1 — Stl — S1 — L L,無法直接實現限界檢測。限界檢測採用的是邏輯系統的限界語義，這與全局檢測採用的無界語義存在很大的不同。因此與謂詞抽象、偏序歸約等約簡技術一樣，在PRISM中為實現限界檢測算法必須大量修改PRISM的原始碼，並重新編譯以實現步長限制下各種概率度量的近似計算。PRISM的源程序目前包含20個文件夾，平均每個文件夾包含20個文件，要具備修改PRISM原始碼的能力必須熟悉這400個左右的文件，而且掌握近1000個函數之間的相互調用關係，因此修改PRISM原始碼是非常困難的，這使得在PRISM上執行限界檢測算法的可操作性很差，而
且工作量巨大。
發明內容
本發明的目的在於提供一種面向限界檢測技術的系統模型構造方法，以提高在PRISM上執行限界檢測技術的可操作性，降低工作量，同時保證利用限界檢測技術約簡狀態空間的效果。為了解決以上技術問題，本發明的採用的技術方案如下。一種面向限界檢測技術的系統模型構造方法，其特徵在於包括以下步驟步驟一，設整數k為所需構造的局部空間的深度，在建模語言的全局變量聲明處引入一個新的全局變量newv,並設置成整數型，初始值為O,即添加語句newv: [O. . k]initO ；步驟二，對語言中的每一條命令，依據符號「 + 」表示的概率分布進行分解，具體分解規則如下 原始命令
權利要求
1.一種面向限界檢測技術的系統模型構造方法，其特徵在於包括以下步驟步驟一，設整數k為所需構造的局部空間的深度，在建模語言的全局變量聲明處引入一個新的全局變量newv,並設置成整數型,初始值為0,即添加語句newv :
init 0 ；步驟二，對語言中的每一條命令，依據符號「 + 」表示的概率分布進行分解，具體分解規則如下原始命令[]guard_l -> prob_l : update_l + . . . + prob_n : update_n 分解後的命令[]guard_l -> prob_l : update_l ；[]guard_l -> prob_2 : update_2 ；......[]guard_l -> prob_n : update_n ；步驟三，對每一個模塊，依據各命令中值為真的謂詞的數量以及謂詞之間組合的不同重新構造模型；步驟四，為了防止出現死循環，在每一個模塊的末尾添加如下命令newV=k-> newv， =newv ；步驟五，將所有模塊重新組合在一起構成新的建模語言。
2.如權利要求1所述的一種面向限界檢測技術的系統模型構造方法，其特徵在於，所述步驟三進一步具體為不失一般性，每一個模塊當中的建模語言抽象如下 module M[]guard_l -> prob_l : update_l ；[]guard_2 -> prob_2 : update_2 ；......[]guard_m -> prob_m : update_m ；Endmodule按下述方法重新構造模型步驟(一)，對每一個update_i (1≤ i≤m),標識出其中被賦值的變量集合V_i,記為V_ i={v_{i, 1}, ···, v_{i, j}},對每個變量 v_{i,h} (I ≤ h ≤ j)，引入記號 f (v_{i,h})表示 update」中對v_{i, h}的賦值操作；步驟(二)，依據謂詞guard_l，……，guarcLm中值為真的謂詞的數量以及謂詞之間組合的不同分別添加命令，新命令中謂詞是三個部分的合取1)值為真的謂詞保持不變；2) 值為假的謂詞取其否定；3)對於任意謂詞值為真的兩條命令，令第一條命令對變量的賦值等於第二條命令對變量的賦值來構建新謂詞；轉換概率是所有謂詞值為真的命令中轉換概率之和；新命令中變量賦值部分從謂詞為真的命令中隨機選擇；步驟(三)，刪除模塊中所有的原始命令。
3.如權利要求2所述的一種面向限界檢測技術的系統模型構造方法，其特徵在於所述步驟(二)進一步具體為步驟(I )，只有一個謂詞為真，添加如下命令
全文摘要
本發明涉及一種面向限界檢測技術的系統模型構造方法，是基於概率模型檢測工具PRISM。包括以下步驟對於局部空間搜索深度k，在建模語言的全局變量聲明處引入新的整數型變量newv，初始值為0；對語言中的每一條命令，依據符號「+」表示的概率分布將其分解成若干只包含一條賦值語句的命令；依據各命令中值為真的謂詞數量以及謂詞之間組合的不同分別添加新命令。新命令中謂詞是三個部分的合取值為真的謂詞保持不變；值為假的謂詞取其否定；對於任意謂詞值為真的兩條命令，令第一條命令對變量的賦值等於第二條命令對變量的賦值來構建新謂詞。本發明可實施性強，工作量小，且保證了利用限界檢測技術約簡狀態空間的效果，可應用於隨機系統建模。
文檔編號G06F9/44GK103049277SQ20131003473
公開日2013年4月17日 申請日期2013年1月29日 優先權日2013年1月29日
發明者周從華 申請人:江蘇大學