基于Petri網的概念模型驗證方法研究

摘 要:針對目前概念模型動態部分內容的驗證由于其復雜性難以通過閱讀式地審查發現其中的瑕疵等問題，提出了利用Petri網進行概念模型驗證的一種新思路，研究了進行概念模型驗證的具體步驟，分析了概念模型錯誤對應的Petri網錯誤，以及檢測這些錯誤時需要驗證的Petri網性質;最后以防空導彈作戰過程為例，研究了利用Petri網以及CPN Tools軟件進行概念模型動態部分內容驗證的具體過程。實踐證明此方法減少了領域專家直接進行概念模型驗證的主觀性影響，提高了效率。

關鍵詞: Petri 網; 概念模型驗證; CPN Tools; 防空導彈作戰過程

中圖分類號:TP391.9 文獻標志碼:A

文章編號:1001-3695(2010)03-0999-03

doi:10.3969/j.issn.1001-3695.2010.03.052

Study of conceptional model validation method based on Petri net

FAN Hao， HUANG Shu-cai

(Missile Institute AFEU， Sanyuan Shaanxi 713800， China)

Abstract:It is difficult to validate the dynamic part of conceptual model by subjective detection in view of its complexity. This paper put forward a new method to validate conceptual model with Petri net. It studied the concrete approaches carrying on the conceptual model validation， analysed the faults of Petri net correlatived with conceptual model and the validated properties of Petri net when detecting these faults. Lastly， as the air defense missile operation process an example， it researched that how to validate the dynamic part of conceptional model with the Petri net and CPN Tools. The practice proves the method’s availability in aspect of reducing the subjective impacts of validating the concetual model directively and improving the efficiency of the validation.

Key words:Petri net; conceptional model validation; CPN Tools; air defense missile operation process

仿真系統概念模型是建模過程中的第一階段，對指導仿真系統的開發和評估具有重要意義[1]。概念模型的正確性是其質量的基本保證，只有正確的概念模型才能真實地反映客觀世界，才能實現高可信度的仿真，才能使仿真設計和實現階段犯錯誤的可能性越小，所以必須對概念模型的正確性進行驗證，以確保概念模型對現實世界問題的模型表達是否能合理地滿足建模目的，從而保證建模和仿真正確進行。

進行概念模型驗證前必須對其進行描述，概念模型的描述可分為格式化描述和形式化描述兩個階段。目前概念模型驗證主要在概念模型描述的基礎上由領域專家對其靜態和動態部分內容進行定性、主觀地審查，以確定概念模型的正確性，這種方法稱之為專家法。概念模型靜態部分的內容比較容易理解和檢查，而動態部分的內容則由于其復雜性難以通過閱讀式地審查發現其中的瑕疵。Gervasi等人[2]提出了輕量級形式化方法的思想，這種思想只能對概念模型的部分關鍵內容進行驗證，而且對其進行形式化描述仍然不是一件容易的事情，有待進一步的研究。文獻[3]提出了利用概念執行機制通過模型的動態執行來發現模型的錯誤或缺陷的方法，并給出了一個基本步驟，但實際操作還存在很大困難。文獻[4，5]指出利用可執行模型在人機交互條件下驗證概念模型的動態部分是很有意義的，但沒有給出具體實施方法。概念模型的驗證是一種流程邏輯的驗證，雖然基于IDEF、UML形式化描述的模型已經很完備，卻不能動態執行。Petri網(尤其是著色Petri網、隨機Petri網等高級Petri網)在流程邏輯驗證方面顯示出了巨大的優勢，它綜合了數據流、控制流和狀態轉移，能很自然地描述并發、同步、資源爭用等特性，而且本身自含執行控制機制，集規范表示與執行于同一模型，并且能夠進行動態仿真等諸多優點，所以用其進行概念模型的驗證將是有意義的。

1 基于Petri網的概念模型驗證步驟

遵循概念模型的驗證貫穿于其開發的全過程這個原則，對一個軍事仿真系統的概念模型進行驗證時，一個可行且易于實際操作的具體驗證步驟如下:

a)獲得概念模型的格式化描述。格式化描述主要解決軍事知識的規范表示，為軍事人員和技術人員提供溝通與合作的橋梁，從而極大地提高了技術開發人員對軍事問題的深入準確理解。

b)獲得概念模型的形式化描述。首先綜合利用直觀易懂的IDEF、UML等建模語言在格式化描述的基礎上進行形式化描述，以更利于理解和下一步的仿真軟件分析設計。通常用IDEF建立系統功能模型，以側重從軍事角度描述系統的功能結構和信息流;用UML用例圖進行系統需求分析，用UML活動圖描述系統行為狀態過程，以側重從技術開發角度描述對系統的認識和理解;然后，把IDEF和UML建立的模型進行映射，得到Petri網動態模型。

c)分析Petri網動態模型。分析Petri網的性質，并利用CPN Tools仿真軟件對建立的Petri網模型進行動態模擬仿真。其中除了可以對標記的流動進行分析外，CPN Tools還可以生成Petri網模型的狀態空間統計信息，包含了Petri網模型的許多性質，這些性質可以輔助概念模型的檢查。

d)進行概念模型驗證。首先進行靜態部分內容的檢查，然后利用步驟c)得到分析結果和信息，輔助軍事專家進行動態部分內容的檢查，根據錯誤情況不斷修改完善系統的概念模型。

2 基于Petri網的概念模型驗證內容

概念模型的描述和客觀世界不一致、對客觀世界的描述不夠完整細致、描述了與仿真應用無關的內容，以及不符合仿真需求目的等都可以視為是影響概念模型正確性和質量的主要因素，反映在其Petri網模型中可使Petri網模型導致以下錯誤[6]:(a)任務沒有輸入和(或)輸出條件，如果任務沒有輸入條件，就不清楚什么時候執行它;如果任務沒有輸出條件，它對事件的完成就不會有任何貢獻，可以被丟棄;(b)死任務，任務永遠不能被執行;(c)死鎖，在事件結束前發生了阻塞;(d)活鎖，把事件帶進無休止的循環;(e)事件結束后，仍有活動執行;(f)事件結束后，定義的過程中仍然存在標記。

由于Petri網錯誤反映了其對應概念模型可能出現的錯誤，通過分析Petri網的性質來發現其錯誤，從而發現概念模型的錯誤。下面給出對概念模型正確性有較大影響的Petri網的性質描述[7]:

a)可達性。用于驗證系統能否達到某種狀態，也就是概念模型是否完全描述了現實世界，對現實世界的描述是否細致，是否能滿足系統需求和仿真應用目的等。

b)有界性。保證了系統的活動在某個操作階段不會堆積。

c)活性。保證了系統不會出現死鎖，過程能正常繼續進行。

d)回歸性(家態)。反映了系統的周期性。

e)公平性。保證了系統運行過程中的每一個進程在資源競爭中不會出現饑餓現象，公平性分析可以幫助找出關鍵變遷，解決系統瓶頸問題。

3 應用實例

3.1 防空導彈武器系統作戰過程描述[8]

防空導彈武器系統的作戰過程為:由上級指揮中心、目標指示雷達、低空補盲雷達這三個通道得到目標流信息，然后送給制導雷達。當指揮自動化系統指揮時，由上級指揮中心負責傳遞目標流信息;當指揮自動化系統損壞或者防空導彈C3I系統獨立作戰時，由目標指示雷達獲取目標流信息;當目標為低空目標時，由低空補盲雷達作進一步搜索。制導雷達獲得目標指示后，進行目標的搜索跟蹤，接著由指控計算機進行目標識別、威脅評估、攔截適宜性檢查、目標分配等(同時可由指揮員進行干預)，接著發射導彈，制導雷達對導彈進行制導，導彈飛行一定距離后，由導彈自主制導，然后實施攔截，最后由制導雷達進行殺傷效果評估。

3.2 作戰過程的Petri網模型[8]

防空導彈武器系統作戰過程是一種典型的離散事件系統，通過把其作戰過程UML活動圖、IDEF功能圖等進行映射，建立其基本Petri網模型，如圖1所示。

該Petri網模型中，資源庫所為R1，R2，R3，R4，R5，R6，R7，R8，分別對應為上級指揮中心、目標指示雷達、低空補盲雷達、制導雷達、指揮員、指控計算機、發射單元、導彈導引頭。它們提供資源，只有忙或閑兩種狀態。

操作庫所的含義描述為p0:來襲目標;p1:目標等待搜索;p2:上級指揮中心傳遞的目標信息;p3:目標指示雷達傳遞的目標信息;p4:目標信息等待輸入制導雷達;p5:搜索的低空目標信息;p6:制導雷達搜索、跟蹤的目標信息;p7:發射決策;p8:發射諸元信息;p9:導彈等待截獲、跟蹤;p10:導彈程序飛行，等待制導;p11:導彈制導飛行;p12:導彈自導引飛行;p13:制導雷達進行殺傷效果評估;p14:殺傷效果評估信息。

Petri網模型中變遷的含義描述為t1:目標到達;t2:上級指揮中心傳遞目標信息;t3:目標指示雷達開始搜索;t4:獲得上級指揮中心傳遞的目標信息;t5:獲得目標指示雷達傳遞的目標信息;t6:低空補盲雷達開始對低空目標進行搜索;t7:制導雷達對目標進行搜索、跟蹤;t8:制導雷達對低空目標進行搜索、跟蹤;t9:指揮員和指控計算機開始進行目標識別、威脅評估、攔截可行性計算和目標分配及計算發射諸元;t10:裝訂發射諸元;t11:不適宜攔截;t12:發射導彈;t13:制導雷達截獲、跟蹤導彈;t14:制導雷達開始對導彈進行制導;t15:導引頭開始自導引導彈飛行;t16:(自導引結束)制導雷達開始進行殺傷效果評估;t17:攔截評估結束;t18:完成攔截任務;t19:進行第二次攔截。

下面分析如何利用Petri網性質和CPN Tools軟件檢驗其Petri網模型的正確性，繼而進行概念模型的驗證。

3.3 進行模型驗證[8]

3.3.1 利用Petri網性質進行分析

1)驗證可達性 分析可達性目的是要知道從初始狀態可以變化到哪些狀態;或給定一狀態，是否可以實施一系列變遷從初始狀態到達該狀態，從而檢驗系統能否順利地進行以及系統是否有死任務。研究Petri網的可達性首先要將所有可達的標志構造出來，即給出可達標志集，然后構造可達標志圖。用Petri網模擬一個防空導彈作戰過程，可達標志集R(M0)給出了作戰過程可能出現的全部狀態。根據其運行規則，可達標志集R(M0)如表1所示。

表1 導彈作戰飛行過程Petri網模型可達標志集

MiR(M0)[p0p1p2p3p4p5p6p7p8p9p10p11p12p13p14R1R2R3R4R5R6R7R8]MiR(M0)[p0p1p2p3p4p5p6p7p8p9p10p11p12p13p14R1R2R3R4R5R6R7R8]

M0[10000000000000011111111]M8[00000000100000011110011]

M1[01000000000000011111111]M9[00000000010000011111101]

M2[00100000000000001111111]M10[00000000001000011101011]

M3 [00010000000000010111111]M11[00000000000100011101011]

M4[00001000000000011111111]M12[00000000000010011111110]

M5[00000100000000011011111]M13[00000000000001011101111]

M6[00000010000000011101111]M14[00000000000000111111111]

M7[00000001000000011110011]

在可達標志集的基礎上，構造所建防空導彈作戰過程Petri網的可達標志圖，如圖2所示。

分析該Petri網的可達標志集和可達標志圖可知:

(a)可達標志集為有限的，說明體系中各物理實體(設備)處理能力能夠保證任務的執行而不至于癱瘓;

(b)在給定初始標志下，圖4中的系統從初始狀態可以到達最終狀態，意味著導彈作戰飛行流程可以順利進行，可達圖恰當地描述了導彈作戰飛行過程。

2)驗證有界性和安全性 由Petri網模型易知，所建模型不但是有界的而且是安全的。同時應該注意到對于具有多目標打擊能力的第3代防空導彈武器系統來說，對應的Petri網模型將不再是安全的，但它依然是有界的。

3)驗證活性 根據可達標志集和可達標志圖易知該網是活的。表明了所建模型不會出現死鎖，整個作戰飛行過程可以正常繼續進行。

4)驗證回歸性(家態) 易知該Petri網模型具有可逆性，充分體現了導彈作戰飛行過程的戰前準備、攔截實施、再戰準備的循環過程。

5)驗證公平性 由于所建Petri網中并發的變遷按一定的隨機概率激發，以解決并發沖突造成的資源競爭。例如對于變遷t18、t19的實施是由一定的概率實施，所以當變遷t18不引發，而另一個變遷t19引發的最大次數是有界的，即t18、t19具有有界—公平關系，同理可知網中的每一個變遷都具有有界—公平關系，則該網是有界—公平網。體現了作戰過程在資源(設備)競爭中不會出現饑餓現象。

綜合以上分析可知，用Petri網建立的導彈作戰過程概念模型是合理的，滿足建模需求。

3.3.2 利用CPN Tools軟件進行分析[9～11]

1)作戰過程的Petri網仿真模型 根據導彈作戰過程的特點，利用CPN Tools軟件建立其Petri網仿真模型時，為了實現其作戰過程并發事件、隨機事件和延時事件的準確描述，以及避免直接建立選擇性結構的Petri網模型會出現并發沖突的資源競爭，并簡化Petri網的圖形表示，擴大標記所擁有的信息量。本文采用廣義隨機著色Petri網來建立其作戰過程層次化模型。該模型由五頁Petri網模型組成，其頂層模型Missile_Process如圖3所示。

頂層Petri網模型的四個變遷擴展為四個子頁，分別Search_Track、Command_Decision、Guidance_Control和Shooting_Evaluate子頁，每個子頁都有自己完整的Petri網模型，這里只給出Search_Track子頁模型，如圖4所示。

其中模型的主要著色集、函數及變量定義如下:

colset RND=int with 1..10;

colset STATE = with wait|arrive|supcom|targetradar|lowattradar|guidradar|C3I|cann'tlau|bindpara|laumissile|trackmissile|guidmissile|selfguidmissile|startevaluate|finishevaluate|finishkill|killagain;

colset TARGET=product STRING*RND*STATE timed;

fun Exp(t:real)=floor(exponential(1.0/t));

fun Uni(a:real，b:real)=floor (uniform(a:real，b:real));

var TarSty:STRING;

var r，r1，r2，r3，r4，r5，r6，r7，r8:BOOL;

var rnd:RND;var i:INT;var state:STATE;

以上著色集中，RND表示1~10的離散隨機整數。STATE是枚舉型數據，表示作戰過程狀態，如selfguidmissile表示導彈自導引階段。TARGET表示庫所的數據類型，是由復合(STRING，RND，STATE)數據類型構成的，STRING表示目標類型，如plane。RND控制隨機變遷的發生，STATE用于跟蹤作戰運行到哪一階段。這里采用隨機數控制并發變遷的激發，以解決并發沖突造成的資源競爭，例如t1變遷輸出產生隨機數，對于t2、t3并發變遷，當隨機數rnd≤7，則變遷t2激發，即由上級指揮中心傳遞目標信息，當rnd>7，則變遷t3激發，即由目標指示雷達傳遞信息。其中當資源庫所中含有BOOL類型的變量true標記時，表示其處于閑狀態，不含標記時，表示其處于忙狀態。函數Exp()及Uni()表示變遷與隨機分布的實施延時相關聯。

2)仿真分析[12] 綜合利用CPN Tools生成的狀態空間報告加之對仿真模型進行單步或連續的模擬仿真，觀察標記的流動可以找出使標記錯誤流動以及不能流動的原因，根據此方法可以檢查出Petri網的大部分錯誤。技術人員把分析結果交給領域專家，輔助領域專家檢測概念模型的描述和現實世界不一致，以及對現實世界的描述不夠細致、不符合仿真目的的錯誤，從而進行模型的修改和完善，這樣減少了專家直接進行概念模型驗證主觀因素的影響，提高了在建模階段發現錯誤的概率。這種方法可以輔助專家發現不易發現的錯誤，提高概念模型驗證的效率。

4 結束語

概念模型驗證是建模與仿真過程中最重要、最困難的問題之一，是仿真系統置信度評估中舉足輕重的一個環節，對提高大型仿真系統的互操作性和可重用性都有著重要意義。通過建立系統Petri網模型，同時利用CPN Tools仿真軟件對其仿真模型進行動態分析，將得到的有關系統結構和動態行為方面的結論和信息提供給專家，輔助專家進行概念模型的檢查，繼而對概念模型進行修改和完善，并且還可以減弱專家主觀性的影響和充分發揮專家評估方法的靈活性，提高概念模型驗證的效率。本文的研究為進行概念模型動態部分內容的驗證提供了有效方法。

參考文獻:

[1] 王子才，王勇.復雜系統仿真概念模型研究進展及方向[J].宇航學報，2007，28(4):779-784.

[2]GERVASI V，NUSEIBEH B. Lightweight validation of natural language requirements[J]. Software Practice and Experience (S0038-0644)，2002，32:113-133.

[3]何曉曄，吳永波，徐培德，等.任務空間概念模型VVA研究[J].火力與指揮控制，2006，31(3):34-37.

[4]郝靖，畢學軍，曹偉華.概念模型驗證[J].四川兵工學報，2008，29(5):144.

[5]易鋒.概念模型的結構化表示[D].武漢:華中科技大學，2006.

[6]AAKST Wil van D，VAN HEE K.工作流管理-模型、方法和系統[M] .王建民，聞立杰，等譯.北京:清華大學出版社，2004.

[7]吳哲輝. Petri網導論[M].北京:機械工業出版社，2006.

[8]龍光正. 防空導彈C3I系統謂詞/變遷賦色Petri網建模與仿真[J].系統工程與電子技術，2002，24(12):47-48.

[9]林闖. 隨機Petri網和系統性能評價[M].北京:清華大學出版社，2005.

[10]GORDON S， BILLINGTON J. Analyzing a missile simulator with co-lored Petri nets[C]//Proc of International Journal on Software Tool for Technology Transfer.[S.l.]:Springer-Verlag，1998:144-159.

[11]魯曉春. 物流系統著色Petri網模型研究[D].北京:北京交通大學，2008.

[12]Analysinga CP-net syntaxcheck， simulation， statespace analysis[EB/OL]. http:// wiki.daimi.au.dk / cpntools-help/ analysing_ a_ cp-net.wiki?cmd=getanchor=Analysing+a+CP-net.