[發明專利]基于Petri網模型的系統仿真驗證方法

在審

• 申請號: 201710486867.6
• 申請日: 2017-06-23
• 公開（公告）號: CN107301128A
• 公開（公告）日: 2017-10-27
• 發明（設計）人: 陳靜;王泊涵;干新源;柯文俊;高昕睿;馮大成
• 申請（專利權）人: 北京計算機技術及應用研究所
• 主分類號: G06F11/36
• 分類號: G06F11/36;G06F17/50
• 代理公司: 中國兵器工業集團公司專利中心11011
• 代理人: 劉東升

技術領域

本發明涉及系統工程建模技術領域，具體涉及一種基于Petri網模型的系統仿真驗證方法。

背景技術

現今，在軟件開發過程中，隨著軟件開發的規模越來越大，復雜度越來越高，一個非常重要的主題就是確保軟件的可靠性和安全性。作為系統工程領域中的重要方法，SysML有著廣泛的應用。它作為系統工程的標準建模語言，能夠支持各種復雜系統的詳細說明、分析、設計、驗證和確認。SysML繼承了UML2的部分視圖，根據需要修改了UML2的部分視圖，同時又增加了需求圖和參數圖。

SysML是一種半形式化的語言描述規范，即沒有明確的語義，在通俗易懂的同時，也使得SysML難以找到可靠的驗證手段。在模型規模越來越大的背景下，包括SysML的主要行為模型活動圖在內，應用常規的人工模型測試，效率會變得非常低下。同時，如果在上層實現過程中發現了軟件設計的缺陷或錯誤，將導致大量的時間消耗和重復工作，例如審查設計和重新實現等。

發明內容

(一)要解決的技術問題

本發明要解決的技術問題是：如何提高系統工程模型仿真效率。(二)技術方案

為了解決上述技術問題，本發明提供了一種基于Petri網模型的系統仿真驗證方法，包括以下步驟：

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

步驟二、利用PIPE工具對Petri網模型進行仿真；

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

優選地，所述控制流的轉換規則為：將SysML活動圖模型中的控制流對應為Petri網中的有向??；

所述動作的轉換規則為：將SysML活動圖模型中的動作對應Petri網中的變遷，同時用Petri網中的一個庫所記錄系統經所述動作改變之后的狀態值；

所述初始節點的轉換規則為：將SysML活動圖模型中的初始節點對應為Petri網中的一個庫所，其值是系統的初始狀態值；

所述結束節點的轉換規則為：將SysML活動圖模型中的結束節點對應為Petri網中的一個庫所，同時用Petri網中的變遷表示進入結束時的狀態變化；

所述分叉節點的轉換規則為：用Petri網中的一個變遷表示作為輸入流的有向弧進入了分叉狀態，同時用多個庫所記錄分叉之后的狀態；

所述結合節點的轉換規則為：用Petri網中的一個變遷表示作為輸入流的多個有向弧進入了結合狀態，同時用一個庫所，記錄結合之后的狀態；

所述判斷節點的轉換規則為：用Petri網中的一個變遷表示進入判斷狀態，同時用于一個庫所記錄判斷之后系統的狀態，該庫所衍生出多個有向弧，以對應不同的控制流。

優選地，利用PIPE工具使用覆蓋樹算法對Petri網模型進行仿真。

優選地，所述使用覆蓋樹算法對Petri網模型進行仿真的步驟具體為：

2.1、把初始標識當做根節點，并標記為新；標識對應Petri網中的庫所，標識的值代表系統的狀態值；

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

2.3、選擇任意一個標記為新的標識；

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

2.5、若標識沒有遷移可觸發，則可將該標識標記為結束，同時轉入步驟2.2；若該標識存在可觸發的遷移，則對每個遷移執行步驟2.6；

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

優選地，步驟三中驗證Petri網模型的有界性具體為：查看標識中每一個值是否均小于常量，所述常量是庫所的容量，若是，則認為此時的Petri網模型是有界的，驗證不通過，否則認為Petri網模型是無界的。