[發明專利]一種基于路徑的模型檢測方法

無效

• 申請號: 201010117908.2
• 申請日: 2010-03-05
• 公開（公告）號: CN101799842A
• 公開（公告）日: 2010-08-11
• 發明（設計）人: 趙棟;羅軍;王蕾;李姍姍;魏立峰;陳松政;何連躍;唐曉東;黃辰林;丁滟;付松齡;王曉川
• 申請（專利權）人: 中國人民解放軍國防科學技術大學
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 國防科技大學專利服務中心 43202
• 代理人: 郭敏

技術領域

本發明涉及一種模型檢測方法，特別涉及一種基于路徑的模型檢測方法。

背景技術

形式化驗證技術使用嚴格的數學模型分析和驗證系統的正確性，在計算機硬件、通信協議、控制系統、安全認證協議等方面有許多成功的應用。模型檢測是基于模型的形式化驗證的基本方法，是一種對待檢測系統進行建模并自動分析驗證的技術，最早由E.M.Clarke和E.A.Emerson以及J.P.Queille和J.Sifakis分別獨立提出。

模型檢測的基本問題是：把待檢測系統的行為用嚴格的形式化語言描述出來，建成待檢測系統的抽象模型；針對待檢測系統提取出待檢測需求，再把待檢測需求形式化為用邏輯公式表達的屬性規范；再利用模型檢測工具驗證抽象模型是否滿足規范，若不滿足，給出違反屬性規范的反例。因此模型檢測方法要解決的問題是：如何建立抽象模型，如何對抽象模型進行驗證。

傳統的模型檢測方法是基于Kripke結構的，抽象模型是一個由Kripke結構描述的狀態轉換系統，屬性規范是若干時序邏輯公式。Kripke結構描述的是一個非限定狀態轉換系統，可以用一個圖來表示，圖中的節點表示系統可以達到的狀態，有向邊表示狀態的遷移。Kripke結構還定義了一個標記函數，標記出每個狀態下為真的所有原子命題的集合。時序邏輯公式的語義就是基于Kripke結構進行解釋的，Kripke結構在模型檢測中負責描述待檢測系統的行為。從Kripke狀態轉換圖的初始節點出發，將該結構展開成一棵無限高度的樹，樹中的每一條路徑就是待檢測系統的一條狀態轉換序列，它表示待檢測系統可能的一次運行狀況。這棵樹包含了所有可能的路徑。實際應用時，待檢測系統的路徑往往很多很復雜，展開樹的分支較多，計算機的主要工作就是展開這個樹，并遍歷所有可能的路徑，找出是否存在違反屬性規范的路徑。若存在違反屬性規范的路徑，則給出該路徑。

為了使用模型檢測工具進行分析和驗證，建模者需要建立待檢測系統的Kripke結構模型，并在模型的基礎上提出用時序邏輯公式描述的待檢測屬性。建模者需要將待檢測系統運行生命周期可能到達的階段劃分為若干個狀態，并明確標示出所有狀態下系統的相應屬性。這樣，計算機才能完成自動搜索并分析驗證的工作。

具體來說，傳統的模型檢測方法有如下幾個步驟。

步驟1，建立邏輯系統。根據待檢測系統的特點和待檢測屬性的需要，建立一個完整的一階邏輯系統，即定義邏輯系統中的函數符號和謂詞符號，并給出它們的語義。隨后的步驟將基于這個一階邏輯系統定義狀態以及狀態轉換關系和描述待檢測屬性，因此，函數符號和謂詞符號的定義應當滿足待檢測系統的特點和待檢測屬性的需要。

步驟2，構建Kripke狀態轉換圖的節點。把待檢測系統的運行過程劃分成若干階段，每個階段對應待檢測系統的一個狀態，每個狀態對應Kripke狀態轉換圖中的一個節點。在此基礎上，定義若干命題，這些命題是基于第一步建立的一階邏輯系統的，它們的真假反映出每個狀態的特征。

步驟3，定義標記函數。標記函數的定義域是狀態節點的集合，值域是第二步中定義的所有命題的集合的冪集(一個集合的冪集是指該集合所有子集構成的集合)。給定一個狀態，標記函數定義了該狀態下所有為真的命題的集合，即定義了每個狀態下每個命題的真值。在不同的狀態下，這些命題的真值呈現出不同組合。

步驟4，建立狀態轉換規則，即構建Kripke狀態轉換圖中的有向邊。若狀態A到狀態B有一條有向邊，則說明狀態A可以轉換到狀態B。經過前四步建立了一個Kripke結構描述的狀態轉換圖，這就是待檢測系統的抽象模型。

步驟5，展開狀態轉換圖并驗證。以初始狀態節點為根節點，把Kripke狀態轉換圖展開成一棵樹，這棵樹是無限高度的，每一條從根節點到葉子節點的路徑是一條可能的狀態轉換路徑。搜索整棵樹，遍歷所有的路徑，尋找違反待檢測屬性的路徑。如果找到了這樣一條路徑，則說明待檢測系統不滿足屬性規范，這一條路徑就是反例。這一步的工作由計算機完成。

傳統的模型檢測方法要求建模者歸納出待檢測系統所有可能的狀態和狀態轉換關系，即需要建立一張完整的狀態轉換圖，圖中包含所有可能的狀態和狀態轉換關系，然后才能交給計算機進行自動驗證。有些待檢測系統十分復雜，運行階段變化較多，建模往往可以粗略地估計出待檢測系統將會發生怎樣的變化，有可能有哪些狀態，但卻難以把所有狀態完整的列舉出來。有些情況下狀態空間甚至是無限擴張的，根本無法完全列舉出來。這增大了模型檢測的難度，使得模型檢測的應用具有較大的局限性。

發明內容