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

無效

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

1.一種基于路徑的模型檢測方法，其特征在于包括以下步驟：

第一步，根據待檢測系統和待檢測需求的特點定義待檢測系統的狀態，這個狀態即為待檢測系統的抽象模型的狀態；一個狀態是一個多元組，其中的每一元是一個集合或一個關系，任意一個集合或關系的變化都引發狀態的變化；所述集合是待檢測系統中與模型檢測相關的實體對象，所述關系是這些集合之間的對應關系，關系本質上也是集合；隨著待檢測系統的運行，集合中的元素會發生變化，這些變化的集合構成多種組合，每種組合就對應著一個狀態；

第二步，劃分操作類型并定義狀態轉換規則：將待檢測系統中的一個事件定義為一個操作，將操作按操作過程是否相同劃分為多種操作類型，同一類型的操作具有相同的操作過程；操作能引起集合和關系發生變化，因此能夠引起狀態發生轉換；狀態轉換規則是規定在每種操作作用下，構成狀態的每一元如何發生變化的規則，由一系列邏輯公式來描述，每個操作都對應一個邏輯公式；邏輯公式形式是：

∃e1...Een(p(s,s′,e1,...,en))]]>

該公式的含義是：存在e1，...，en使得公式p(s，s’，e1，...，en)為真；其中s是操作前狀態，s’是操作后狀態，p是操作類型對應的謂詞，謂詞至少有兩個參數：操作前狀態s和操作后狀態s’，e1，...，en是額外參數，額外參數是操作所涉及的實體對象的標識；每種操作類型都對應一個謂詞，由建模者根據每種操作在待檢測系統的實際動作分別定義；謂詞是描述額外參數與s，s’之間的關系以及s和s’之間的關系的一個命題，這個命題是一系列子命題的合取式，命題為真當且僅當所有的子命題為真；子命題分為兩類，一類描述額外參數與s和s’之間的關系，另一類描述s和s’之間的關系，即描述構成狀態的每個元對應的集合的元素如何變化；

第三步，生成狀態轉換序列并判定、驗證：

步驟3.1，定義兩種類型的節點：狀態節點和操作節點，其中操作節點根據第二步中劃分的操作類型分為多種，每個操作節點都屬于其中的一種，每個操作節點都對應一種操作類型；

步驟3.2，根據待檢測系統的實際情況和待檢測需求確定初始狀態節點；

步驟3.3，確定初始搜索閾值a0，a0是大于等于3的奇數，令變量a＝a0；

步驟3.4，以初始狀態節點為頭節點，隨機生成一條長度為a的狀態轉換序列，若順利生成，則繼續，否則令a＝a+2，重復步驟3.4；

步驟3.5，判定狀態轉換序列的合法性，同時滿足以下兩個條件的狀態轉換序列判定為合法的：

A1)狀態轉換序列中的節點滿足狀態節點和操作節點交替出現；

A2)對于狀態轉換序列中的任何操作節點op，若其前驅節點為s，后繼節點為s’，op所屬的操作類型為c，在狀態轉換規則中，c對應的謂詞為p，設p的額外參數為e1，...，en，則邏輯公式為真；

若狀態轉換序列不合法則轉步驟3.4，若合法則轉步驟3.6；

步驟3.6，檢查狀態轉換序列是否違反屬性規范，若不違反則轉步驟3.4；若違反，則停止運行，此時找到了待檢測系統中的一條運行路徑，在該運行路徑下，待檢測系統將發生違反待檢測需求的狀況。

2.如權利要求1所述的一種基于路徑的模型檢測方法，其特征在于定義模型狀態時采用Alloy語言描述狀態定義所涉及到的集合和關系，并在此基礎上用Alloy語言給出狀態的定義。

3.如權利要求1所述的一種基于路徑的模型檢測方法，其特征在于描述狀態轉換規則的邏輯公式采用Alloy語言表達。

4.如權利要求1所述的一種基于路徑的模型檢測方法，其特征在于所述狀態轉換序列由Alloy?Analyzer隨機生成。