[發明專利]一種基于MSVL的Petri網模型檢測方法

有效

• 申請號: 201510040674.9
• 申請日: 2015-01-27
• 公開（公告）號: CN104657542B
• 公開（公告）日: 2017-12-19
• 發明（設計）人: 段振華;師亞;田聰;張南;王小兵;黃伯虎
• 申請（專利權）人: 西安電子科技大學
• 主分類號: G06F17/50
• 分類號: G06F17/50
• 代理公司: 北京科億知識產權代理事務所(普通合伙)11350
• 代理人: 湯東鳳

技術領域

本發明屬于Petri網的模型檢測技術領域，尤其涉及一種基于MSVL的Petri網模型檢測方法。

背景技術

作為圖形化和形式化的工具，Petri網被廣泛的應用于建模和分析離散事件系統。Petri網的圖形能夠將復雜的需求直觀地表達出來，而模糊的文本描述或者晦澀的數學符號則不能。除此之外，利用Petri網的數學理論能夠對系統模型的一些性質(例如可達性、安全性和活性)進行形式化分析。現有的Petri網分析方法包括覆蓋樹方法、網化簡方法和網展開方法等。除此之外，針對Petri網現已提出多種模型檢測方法，例如偏序模型檢測、符號模型檢測和限界模型檢測。這些方法可以驗證用線性時序邏輯(LTL)和計算樹邏輯(CTL)描述的性質。雖然這兩個邏輯能描述很廣泛的性質，但是仍然難以滿足實際應用的需要。這是因為它們的描述能力都不是完全正則的。Petri網有順序語意、并行語意和最大并行語意等多種語意，然而現有的模型檢測方法通常只驗證順序語意的性質。因此，目前難以充分驗證Petri網各種語意的完全正則性質。

投影時序邏輯(PTL)是區間時序邏輯(ITL)的擴展，可以用于描述和驗證并發系統。命題投影時序邏輯(PPTL)不僅具有完全正則表達能力，而且擅長描述順序和迭代行為。建模、仿真和驗證語言(MSVL)是PTL的可執行子集，不僅包含順序語句、條件語句和循環語句，還具備并行語句和等待語句。作為形式化程序設計語言，MSVL不但可以像一般的命令式程序設計語言一樣執行，而且可以像Promela語言一樣建模并行系統，還可以利用統一模型檢測方法對PPTL描述的系統性質進行驗證。除此之外，目前MSVL的支持工具MSV已經實現，可以對MSVL程序進行仿真、建模和驗證。

發明內容

本發明的目的在于提供一種基于MSVL的Petri網模型檢測方法，旨在解決現有的Petri網模型檢測方法難以充分驗證各種語意的完全正則性質的問題。

本發明的目的在于提供一種基于MSVL的Petri網模型檢測方法，該基于MSVL的Petri網模型檢測方法首先利用現有的建模工具Workcraft建立Petri網系統模型，然后使用轉換工具PN3MSVL和PN4MSVL將Petri網系統轉換成順序等價、并行等價或最大并行等價的MSVL程序；最后利用現有的MSVL支持工具MSV對生成的MSVL程序進行仿真、建模和驗證。

進一步，該基于MSVL的Petri網模型檢測方法包括以下步驟：

步驟一：利用建模工具Workcraft建立Petri網系統模型；

步驟二：利用轉換工具PN3MSVL和PN4MSVL將Petri網系統轉換成順序等價、并行等價或最大并行等價的MSVL程序；

步驟三：利用MSVL支持工具MSV對生成的MSVL程序進行仿真、建模和驗證。

進一步，Workcraft、PN3MSVL、PN4MSVL和MSV已經集成到工具集MSVToolkit中。

進一步，步驟二中PN3MSVL實現了順序語意指導的轉換；首先通過解析g文件來構造Petri網系統Z＝(P,T,W,M₀)，g文件由Workcraft建模生成；然后將Z轉換為順序等價的MSVL程序并將顯示在MSVToolkit的文本框內：

其中對每個變遷t∈T，g_t≡∧_q∈Pv_q≥w_qt和對每個庫所q∈P，m_q＝M₀(q)是自然數；對每個庫所w_qt＝W(q,t)和w_tq＝W(t,q)都是自然數；另外，g_T≡∨_t∈Tg_t。

進一步，步驟二中PN4MSVL實現了并行語意指導的轉換和最大并行語意指導的轉換；首先通過解析g文件來構造安全的Petri網系統Z＝(P,T,W,M₀)，g文件由Workcraft建模生成；然后將Z轉換為并行等價的MSVL程序或最大并行等價的MSVL程序并將程序顯示在MSVToolkit的文本框內：

其中g_T的定義與MSVL程序中的相同，

進一步，步驟三中利用工具MSV分別對和進行仿真、建模和驗證。

進一步，利用MSV分別仿真執行和從而得到Z的一個最小步字、步字和最大步字。