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

無效

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

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

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

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

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

分解后的命令：

[]?guard_1?->?prob_1?:?update_1；

[]?guard_1?->?prob_2?:?update_2；

……

[]?guard_1?->?prob_n?:?update_n；

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

步驟四,為了防止出現死循環，在每一個模塊的末尾添加如下命令：?newv=k->?newv’=newv；

步驟五,將所有模塊重新組合在一起構成新的建模語言。

2.如權利要求1所述的一種面向限界檢測技術的系統模型構造方法，其特征在于，所述步驟三進一步具體為：

不失一般性，每一個模塊當中的建模語言抽象如下

module?M

[]?guard_1?->?prob_1?:?update_1；

[]?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}(1≤h≤j)，引入記號f(v_{i，h})表示update_i中對v_{i，h}的賦值操作；

步驟（二），依據謂詞guard_1，……，guard_m中值為真的謂詞的數量以及謂詞之間組合的不同分別添加命令，新命令中謂詞是三個部分的合取：1)值為真的謂詞保持不變；2）值為假的謂詞取其否定；3）對于任意謂詞值為真的兩條命令，令第一條命令對變量的賦值等于第二條命令對變量的賦值來構建新謂詞；轉換概率是所有謂詞值為真的命令中轉換概率之和；新命令中變量賦值部分從謂詞為真的命令中隨機選擇；

步驟(三)，刪除模塊中所有的原始命令。

3.如權利要求2所述的一種面向限界檢測技術的系統模型構造方法，其特征在于所述步驟(二)進一步具體為：

步驟（1），只有一個謂詞為真，添加如下命令：

//?guard_1為真，其余為假（“//”表示此語句僅起注釋作用）

[]?guard_1&!?guard_2&…&!?guard_m?->?prob_1?:?update_1&newv’=newv+1；

//?guard_2為真，其余為假

[]?!guard_1&?guard_2&!?guard_3&…&!?guard_m?->?prob_2?:?update_2&newv’=newv+1；

……

//?guard_m為真，其余為假

[]!guard_1&?!guard_2&……&!guard_(m-1)&?guard_m?->?prob_m?:?update_m&newv’=newv+1；

????步驟（2），兩個謂詞為真，其余為假，添加如下命令：

???????//?guard_1，guard_2為真，其余為假，且V_1=V_2

[]?guard_1&?guard_2&?！guard_3&……&!?guard_m?&?(f(v_{1，1})=f(?v_{2，1}))&?……&(f(v_{1，j})=f(?v_{2，j}))->?prob_1+?prob_2?:?update_1??&newv’=newv+1；

//?guard_1，guard_3為真，其余為假，且V_1=V_3

[]?guard_1&?guard_3&!?guard_2&…&!?guard_m?&?(f(v_{1，1})=f(?v_{3，1}))&?……&(f(v_{1，j})=f(?v_{3，j}))->?prob_1+?prob_3?:?update_1&newv’=newv+1；

……

//?guard_(m-1)，guard_m為真，其余為假，且V_(m-1)=V_m

[]!guard_1&?…&!?guard_{m-2}&guard_(m-1)&?guard_m?&?(f(v_{m-1，1})=f(?v_{m，1}))

&?……&(f(v_{m-1，j})=f(?v_{m，j}))->prob_(m-1)+?prob_m?:?update_(m-1)&newv’=newv+1；

步驟（3），三個謂詞為真，其余為假，添加如下命令：

//?guard_1，guard_2，guard_3為真，其余為假，且V_1=V_2=V_3

[]?guard_1&?guard_2&guard_3&!?guard_4&…&!?guard_m?&?(f(v_{1，1})=f(?v_{2，1}))&?……&(f(v_{1，j})=f(?v_{2，j}))&?(f(v_{2，1})=f(?v_{3，1}))&?……&(f(v_{2，j})=f(?v_{3，j}))->?prob_1+?prob_2+?prob_3?:?update_1&newv’=newv+1；

……

//?guard_(m-2)，guard_(m-1)，guard_m為真，其余為假，且V_(m-2)=V_(m-1)=V_m

[]?!guard_1&?!guard_2&…&!guard_(m-3)&guard_(m-2)&?guard_(m-1)&guard_(m)?&?(f(v_{m-2，1})=f(?v_{m-1，1}))&?……&(f(v_{m-2，j})=f(?v_{m-1，j}))&?(f(v_{m-1，1})=f(?v_{m，1}))&?……&(f(v_{m-1，j})=f(?v_{m，j}))->?prob_(m-2)+?prob_(m-1)+?prob_m??:?update_(m-1)&newv’=newv+1；

????依此類推到步驟（m），這里m是模塊中所含謂詞的個數，

????步驟（m），m個謂詞為真且V_1=V_2=……=V_m，添加如下命令：

//?guard_1，……，guard_m為真，且V_1=……=V_m

[]?guard_1&?guard_2&guard_3&guard_4&…&?guard_m?&?(f(v_{1，1})=f(?v_{2，1}))&?……&(f(v_{1，j})=f(?v_{2，j}))&?(f(v_{2，1})=f(?v_{3，1}))&?……&(f(v_{2，j})=f(?v_{3，j}))&?……&(f(v_{m-1，1})=f(?v_{m，1}))&?……&(f(v_{m-1，j})=f(?v_{m，j}))->?prob_1+?prob_2+……+?prob_m?:?update_1&newv’=newv+1。