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

有效

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

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

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)是自然數；對每個庫所q∈·t·，w_qt＝W(q,t)和w_tq＝W(t,q)都是自然數；另外，g_T≡∨_t∈Tg_t；P和T是兩個有限非空且不相交的集合，分別稱作庫所集合和變遷集合；Petri網系統是四元組Z＝(P,T,F,M₀)，其中(P,T,F)是Petri網，M₀是Petri網系統的初始標識；變量v_q用于記錄庫所q中的托肯數量。

2.如權利要求1所述的基于MSVL的Petri網模型檢測方法，其特征在于，Workcraft、PN3MSVL、PN4MSVL和MSV已經集成到工具集MSVToolkit中。

3.如權利要求1所述的基于MSVL的Petri網模型檢測方法，其特征在于，PN4MSVL實現了并行語意指導的轉換和最大并行語意指導的轉換；首先通過解析g文件來構造安全的Petri網系統Z＝(P,T,W,M₀)，g文件由Workcraft建模生成；然后將Z轉換為并行等價的MSVL程序或最大并行等價的MSVL程序并將程序顯示在MSVToolkit的文本框內：

其中g_T和為順序等價的MSVL程序P和T是兩個有限非空且不相交的集合，分別稱作庫所集合和變遷集合；Petri網系統是四元組Z＝(P,T,F,M₀)，其中(P,T,F)是Petri網，M₀是Petri網系統的初始標識；變量v_q用于記錄庫所q中的托肯數量；變量v_t用于標記變遷t是否在當前標識下執行；m_q＝M₀(q)是自然數。

4.如權利要求1所述的基于MSVL的Petri網模型檢測方法，其特征在于，利用工具MSV分別對和進行仿真、建模和驗證；為順序等價的MSVL程序；并行等價的MSVL程序最大并行等價的MSVL程序

5.如權利要求4所述的基于MSVL的Petri網模型檢測方法，其特征在于，利用MSV分別仿真執行和得到Z的一個最小步字、步字和最大步字；為順序等價的MSVL程序；并行等價的MSVL程序最大并行等價的MSVL程序

6.如權利要求4所述的基于MSVL的Petri網模型檢測方法，其特征在于，利用MSV分別構造和的范式圖，得到Z在順序語意、并行語意和最大并行語意下的狀態空間；為順序等價的MSVL程序；并行等價的MSVL程序最大并行等價的MSVL程序

7.如權利要求4所述的基于MSVL的Petri網模型檢測方法，其特征在于，利用MSV分別驗證和是否滿足PPTL公式描述的完全正則性質，判斷Z的順序語意、并行語意和最大并行語意是否滿足該性質；為順序等價的MSVL程序；并行等價的MSVL程序最大并行等價的MSVL程序