[發(fā)明專利]基于Petri網(wǎng)模型的系統(tǒng)仿真驗證方法

在審

• 申請?zhí)枺?/td>: 201710486867.6
• 申請日: 2017-06-23
• 公開（公告）號: CN107301128A
• 公開（公告）日: 2017-10-27
• 發(fā)明（設(shè)計）人: 陳靜;王泊涵;干新源;柯文俊;高昕睿;馮大成
• 申請（專利權(quán)）人: 北京計算機(jī)技術(shù)及應(yīng)用研究所
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F17/50
• 代理公司: 中國兵器工業(yè)集團(tuán)公司專利中心11011
• 代理人: 劉東升

1.一種基于Petri網(wǎng)模型的系統(tǒng)仿真驗證方法，其特征在于，包括以下步驟：

步驟一、在SysML活動圖模型中，建立元素的轉(zhuǎn)換規(guī)則，從而將SysML活動圖模型在語義不變的前提下轉(zhuǎn)換到Petri網(wǎng)模型，所述元素包括控制流、動作、初始節(jié)點、結(jié)束節(jié)點、分叉節(jié)點、結(jié)合節(jié)點和判斷節(jié)點；

步驟二、利用PIPE工具對Petri網(wǎng)模型進(jìn)行仿真；

步驟三、利用步驟二的仿真結(jié)果驗證Petri網(wǎng)模型的有界性、安全性、活性與無死鎖性，在驗證不通過時根據(jù)需要對Petri網(wǎng)模型進(jìn)行修改，修改之后再重新驗證，直至確定Petri網(wǎng)模型的正確性為止。

2.如權(quán)利要求1所述的方法，其特征在于，所述控制流的轉(zhuǎn)換規(guī)則為：將SysML活動圖模型中的控制流對應(yīng)為Petri網(wǎng)中的有向弧；

所述動作的轉(zhuǎn)換規(guī)則為：將SysML活動圖模型中的動作對應(yīng)Petri網(wǎng)中的變遷，同時用Petri網(wǎng)中的一個庫所記錄系統(tǒng)經(jīng)所述動作改變之后的狀態(tài)值；

所述初始節(jié)點的轉(zhuǎn)換規(guī)則為：將SysML活動圖模型中的初始節(jié)點對應(yīng)為Petri網(wǎng)中的一個庫所，其值是系統(tǒng)的初始狀態(tài)值；

所述結(jié)束節(jié)點的轉(zhuǎn)換規(guī)則為：將SysML活動圖模型中的結(jié)束節(jié)點對應(yīng)為Petri網(wǎng)中的一個庫所，同時用Petri網(wǎng)中的變遷表示進(jìn)入結(jié)束時的狀態(tài)變化；

所述分叉節(jié)點的轉(zhuǎn)換規(guī)則為：用Petri網(wǎng)中的一個變遷表示作為輸入流的有向弧進(jìn)入了分叉狀態(tài)，同時用多個庫所記錄分叉之后的狀態(tài)；

所述結(jié)合節(jié)點的轉(zhuǎn)換規(guī)則為：用Petri網(wǎng)中的一個變遷表示作為輸入流的多個有向弧進(jìn)入了結(jié)合狀態(tài)，同時用一個庫所，記錄結(jié)合之后的狀態(tài)；

所述判斷節(jié)點的轉(zhuǎn)換規(guī)則為：用Petri網(wǎng)中的一個變遷表示進(jìn)入判斷狀態(tài)，同時用于一個庫所記錄判斷之后系統(tǒng)的狀態(tài)，該庫所衍生出多個有向弧，以對應(yīng)不同的控制流。

3.如權(quán)利要求1所述的方法，其特征在于，利用PIPE工具使用覆蓋樹算法對Petri網(wǎng)模型進(jìn)行仿真。

4.如權(quán)利要求1所述的方法，其特征在于，所述使用覆蓋樹算法對Petri網(wǎng)模型進(jìn)行仿真的步驟具體為：

2.1、把初始標(biāo)識當(dāng)做根節(jié)點，并標(biāo)記為新；標(biāo)識對應(yīng)Petri網(wǎng)中的庫所，標(biāo)識的值代表系統(tǒng)的狀態(tài)值；

2.2、判斷是否樹的所有標(biāo)識的標(biāo)記均為不新，如果樹的所有標(biāo)識的標(biāo)記均不為新，則算法結(jié)束，輸出結(jié)果；若存在標(biāo)記為新的標(biāo)識，則執(zhí)行下一步；

2.3、選擇任意一個標(biāo)記為新的標(biāo)識；

2.4、判斷是否有同根的相同標(biāo)識，若從根節(jié)點到該標(biāo)記為新的標(biāo)識的路徑上有相同的標(biāo)識，則將該標(biāo)記為新的標(biāo)識標(biāo)記為舊，再取其他標(biāo)記為新的標(biāo)識；否則執(zhí)行下一步；

2.5、若標(biāo)識沒有遷移可觸發(fā)，則可將該標(biāo)識標(biāo)記為結(jié)束，同時轉(zhuǎn)入步驟2.2；若該標(biāo)識存在可觸發(fā)的遷移，則對每個遷移執(zhí)行步驟2.6；

2.6、確定遷移觸發(fā)標(biāo)識的情況下的后繼標(biāo)識，引入后繼標(biāo)識作為覆蓋樹的一個新節(jié)點，并用遷移標(biāo)注從該標(biāo)識到后繼標(biāo)識的有向弧，同時也將后繼標(biāo)識標(biāo)記為新，返回步驟2.2。

5.如權(quán)利要求1所述的方法，其特征在于，步驟三中驗證Petri網(wǎng)模型的有界性具體為：查看所有標(biāo)識，若標(biāo)識中每一個值是否均小于常量，所述常量是庫所的容量，若是，則認(rèn)為此時的Petri網(wǎng)模型是有界的，驗證不通過，否則認(rèn)為Petri網(wǎng)模型是無界的。

6.如權(quán)利要求1所述的方法，其特征在于，步驟三中驗證Petri網(wǎng)模型的安全性具體為：如果覆蓋樹中的所有標(biāo)識的每一個值都是小于或等于1的，則認(rèn)為Petri網(wǎng)模型是安全的，否則認(rèn)為Petri網(wǎng)模型是不安全的，驗證不通過。

7.如權(quán)利要求1所述的方法，其特征在于，步驟三中驗證Petri網(wǎng)模型的活性與無死鎖性具體為：如果在覆蓋樹中發(fā)現(xiàn)所有變遷都在一個序列中發(fā)生，則認(rèn)為在Petri網(wǎng)模型中不存在死鎖，否則認(rèn)為存在死鎖，驗證不通過。