高江林 吳曉燕

空軍工程大學(xué)導(dǎo)彈學(xué)院，陜西三原 713800

任務(wù)空間概念模型(Conceptual Models of the Mission Space，CMMS)以一種獨立于仿真實現(xiàn)的方式[1]，描述了軍事行動相關(guān)的過程、實體、關(guān)系，成為作戰(zhàn)模擬系統(tǒng)開發(fā)的共同起點和權(quán)威標(biāo)準(zhǔn)，在領(lǐng)域?qū)＜液烷_發(fā)人員之間扮演著橋梁和溝通作用。高質(zhì)量的概念模型需要經(jīng)過反復(fù)的校驗，它是仿真可信度的基礎(chǔ)。由于任務(wù)空間概念模型靜態(tài)部分的內(nèi)容比較容易理解和檢查，而動態(tài)部分的邏輯性、合理性等內(nèi)容則由于行為的復(fù)雜性、缺乏有效的驗證手段成為概念模型校驗的難點和重點。

作為一種定義良好、功能強大的建模語言，UML支持從需求分析開始的系統(tǒng)開發(fā)全過程，已廣泛運用在任務(wù)空間概念模型的建模。為了保證模型的可信度，系統(tǒng)建模后往往還需要進行嚴(yán)格的形式化分析和驗證，而UML是半形式化的語言，難以對關(guān)鍵系統(tǒng)的模型進行語義分析和一致性驗證。采用Petri網(wǎng)進行概念模型形式化分析和驗證是理論和方法研究的重要方向，但對于如何開展驗證工作研究較少。文獻[2-3]研究了如何從UML模型向基于有色Petri網(wǎng)的可執(zhí)行模型轉(zhuǎn)換，并依據(jù)Petri網(wǎng)技術(shù)來分析系統(tǒng)的行為和性能。文獻[4]還提到可以采用狀態(tài)機的形式化描述方法研究軟件動態(tài)體系結(jié)構(gòu)與靜態(tài)體系結(jié)構(gòu)的一致性。由于Petri網(wǎng)尤其是著色Petri網(wǎng)(Colored Petri Nets，CPN)引入了層次化、顏色集和弧上標(biāo)注的概念，非常適合表達復(fù)雜作戰(zhàn)模擬系統(tǒng)，方便分析模型性質(zhì)和仿真模型性能[5]，而且有成熟工具CPNTools[6]和可執(zhí)行的規(guī)格說明工具ExSpect[7]的支持，使得運用Petri網(wǎng)建立概念模型的可執(zhí)行模型，并進行仿真驗證、性能評價變得可行而實用。首先建立基于CPN的動態(tài)行為驗證過程，并論述了動態(tài)行為驗證的主要內(nèi)容，再運用CPN Tools對反導(dǎo)作戰(zhàn)概念模型進行動態(tài)行為驗證。

1 CMMS動態(tài)行為驗證基礎(chǔ)

驗證是指從M&S預(yù)期應(yīng)用角度確定一個模型或仿真系統(tǒng)代表真實世界正確程度的過程。驗證的任務(wù)是根據(jù)特定的建模目的和目標(biāo)，考察模型在其作用域內(nèi)是否準(zhǔn)確地代表了實際系統(tǒng)，確定模型描述真實世界滿足預(yù)定目的的程度，也就是說模型的輸出在多大程度上與實際現(xiàn)象一致，與人們對真實世界相關(guān)對象領(lǐng)域的理解一致，如所表達的任務(wù)空間(軍兵種、戰(zhàn)斗規(guī)模、武器裝備、作戰(zhàn)環(huán)境、實體分辨率等)是否與用戶提供的想定一致，對作戰(zhàn)指揮、作戰(zhàn)行動的簡化是否合理，仿真系統(tǒng)的運行軌跡和流程是否與真實世界相似，仿真結(jié)果與其參照物是否相一致等。

對CMMS動態(tài)行為的驗證主要檢查所建立的動態(tài)模型所表現(xiàn)的動態(tài)行為是否正確、一致，而靜態(tài)校驗方法無法完成這一校驗，因而需要利用可執(zhí)行模型在人機交互條件下實施驗證，即動態(tài)行為的可執(zhí)行驗證。動態(tài)行為的驗證建立在形式化描述的基礎(chǔ)上，一般利用UML時序圖顯示對象之間的交互，反映控制流隨時間推移的可視化軌跡。UML活動圖描述系統(tǒng)行為狀態(tài)過程和各種活動的執(zhí)行順序。不同的描述形式表現(xiàn)系統(tǒng)不同的功能和結(jié)構(gòu)，由于上述形式化描述不能動態(tài)執(zhí)行，驗證時將它們映射為Petri網(wǎng)模型，利用CPN Tools運行模型，按照驗證內(nèi)容進行性能分析，并將結(jié)果反饋校正，不斷修正模型，直到各項性能滿足用戶期望。首先建立基于CPN的動態(tài)行為驗證過程如圖1表示。

圖1 基于CPN的動態(tài)行為驗證過程

2 CMMS動態(tài)行為驗證內(nèi)容

進行動態(tài)行為驗證，主要從正確性和一致性兩個方面來考慮[3]。正確性是驗證概念模型的動態(tài)行為是否正確反映了各對象的行為功能、對象關(guān)系等；一致性主要是驗證不同的行為表現(xiàn)角度在動態(tài)行為上的吻合性。限于篇幅，本文只對采用UML時序圖描述的反導(dǎo)作戰(zhàn)模型進行了正確性驗證。

在驗證正確性時，要根據(jù)目的選擇模型所需滿足的性質(zhì)，當(dāng)Petri網(wǎng)模型表現(xiàn)出一組所需要的性質(zhì)時，就認為概念模型是正確的。Petri網(wǎng)有許多重要性質(zhì)，下面給出對概念模型正確性有較大影響的Petri網(wǎng)的性質(zhì)描述[8]：

1)可達性：從初始標(biāo)識開始，每一個標(biāo)識都可達。用于驗證系統(tǒng)能否達到某種狀態(tài)，也就是概念模型是否完全描述了現(xiàn)實世界，對現(xiàn)實世界的描述是否細致，是否能滿足系統(tǒng)需求和仿真應(yīng)用目的等;

2)有界性：任何庫所的標(biāo)識都是有界的，保證了系統(tǒng)的活動在某個操作階段不會堆積;

3)無死鎖性：不存在死標(biāo)識，意味著系統(tǒng)中不會發(fā)生全局死鎖;

4)活性：從任何可達標(biāo)識開始，每個變遷至少發(fā)生一次;

5)家態(tài)：存在一個從任何其他標(biāo)識都可以到達的標(biāo)識，指出系統(tǒng)可以重新初始化其自身;

6)公平性：無限運行序列的網(wǎng)系統(tǒng)中，如果有一個變遷一直沒有發(fā)生，那么其他所有變遷不可能無限次地發(fā)生。保證了系統(tǒng)運行過程中的每一個進程在資源競爭中不會出現(xiàn)饑餓現(xiàn)象，公平性分析可以幫助找出關(guān)鍵變遷，解決系統(tǒng)瓶頸問題。

3 CPN Tools仿真

各種Petri網(wǎng)(包括高級網(wǎng))工具已開發(fā)多年，CPN Tools是最有代表性的，它由丹麥Aarhus大學(xué)的Jensen教授領(lǐng)導(dǎo)的團隊開發(fā)，專用于CPN的編輯、仿真、分析，其中大量的自動化工具可以方便的進行概念模型動態(tài)行為的校驗。CPN Tools工具的使用主要包括語法校驗、網(wǎng)絡(luò)仿真、狀態(tài)空間分析三部分[9]。

1)語法校驗(Syntax Checking)：當(dāng)用CPN Tools 創(chuàng)建一個CPN或載入一個著色Petri網(wǎng)絡(luò)時，CPN Tools會自動檢測模型數(shù)據(jù)聲明，通過顏色指示判斷檢測是否有語法錯誤。如果有錯誤，光環(huán)的顏色為紅色，可以按照矩形框中顯示的錯誤信息提示進行修改。

2)網(wǎng)絡(luò)仿真(Simulating Nets)：當(dāng)一個CPN成功通過語法檢測后，可以運行仿真程序。仿真運行時，可以實時顯示諸如庫所當(dāng)前標(biāo)示、可觸發(fā)的變遷等反饋信息。仿真過程會記錄在仿真報告中，其中包括有關(guān)變遷觸發(fā)信息的文本。

3)狀態(tài)空間分析：當(dāng)網(wǎng)絡(luò)沒有錯誤，所有庫所、變遷和頁面都有唯一的CPN ML名稱后，可以選擇狀態(tài)空間工具進行分析和計算。進入狀態(tài)空間成功以后，可先后運行“計算狀態(tài)空間”工具和“計算強連接部件圖”工具，之后保存狀態(tài)分析報告，報告內(nèi)容包括有界性、活性、公平性、家態(tài)等，通過分析報告內(nèi)容可以對模型性能進行評估。

4 基于UML的反導(dǎo)作戰(zhàn)概念模型動態(tài)行為驗證

4.1 反導(dǎo)作戰(zhàn)概念模型UML描述

反導(dǎo)作戰(zhàn)系統(tǒng)[10]從功能上可劃分為導(dǎo)彈預(yù)警、指控中心BM/C3I、攔截打擊以及作戰(zhàn)保障4個分系統(tǒng)，對彈道導(dǎo)彈的攔截可沿其飛行全程——助推段、中段(自由段)及至末段(再入段)實施多層攔截。目前，由于技術(shù)手段的限制，末段被認為可行性較高的攔截階段，對于某空天信息支援反導(dǎo)作戰(zhàn)過程，經(jīng)建模分析，建立其末端防御的高低兩層反導(dǎo)作戰(zhàn)時序圖，如圖2所示。

圖2 末段高低兩層反導(dǎo)作戰(zhàn)時序圖

其中，信息流數(shù)據(jù)分別為：

info(1)：BM發(fā)射預(yù)警信息，目標(biāo)彈道的估算數(shù)據(jù)。

info(2)：BM發(fā)射預(yù)警信息，目標(biāo)指示信息。

info(3)：實時目標(biāo)信息，目標(biāo)識別信息，攔截導(dǎo)彈發(fā)射所需數(shù)據(jù)等。

info(4)：目標(biāo)初步指示信息，下達作戰(zhàn)命令。

info(5)：分配攔截的目標(biāo)數(shù)及編號，目標(biāo)指示信息，威脅排序及分配結(jié)果。

info(6)：目標(biāo)指示信息，制導(dǎo)雷達狀態(tài)指令，能量分配控制。

info(7)：目標(biāo)識別信息，導(dǎo)彈發(fā)射裝訂參數(shù)，制導(dǎo)方式轉(zhuǎn)換指令。

info(8)：中段制導(dǎo)指令，殺傷攔截指令。

info(9)：目標(biāo)指示信息，威脅排序及分配結(jié)果。

check：判斷能否進行二次攔截。

feedback(1)：目標(biāo)指示信息，預(yù)警雷達狀態(tài)信息，能量分配控制。

feedback(2,4,5)：狀態(tài)反饋指令，攔截結(jié)果反饋。

feedback(3)：目標(biāo)識別指令，發(fā)射決策、火力分配結(jié)果反饋。

feedback(6)：敵情監(jiān)視指令。

4.2 CPN 模型

根據(jù)圖2所示時序圖模型，建立其CPN 模型，通過計算機仿真驗證模型的正確性。CPN模型的數(shù)據(jù)聲明如下所示，Radar是枚舉顏色集，給出了預(yù)警雷達的早期預(yù)警信息；Bmc3i列舉指揮控制信息；H_c3i，L_c3i顏色集列舉了高低兩層指控中心的目標(biāo)指示信息；H_radar，L_radar顏色集列舉了高低兩層制導(dǎo)雷達的制導(dǎo)信息；H_incept，L_ incept顏色集列舉了高低兩層攔截彈的攔截發(fā)射信息；H_eval，L_ eval則是攔截效果評估信息。其余分別為相應(yīng)顏色集下的變量，以方便弧標(biāo)注和結(jié)構(gòu)控制。

colset Radar=with earlywarn；var warn: Radar；

colset Bmc3i=with target；var tar:Bmc3i；

colset H_c3i=with identify；var iden:H_c3i；

colset H_radar=with order；var inc:H_radar；

colset H_incept=with fashe；var fire,assign,effect:H_incept；

colset H_eval=with success|fail；var eval,waitfed: H_eval；

colset L_c3i=with incept；var fight:L_c3i；

colset L_radar=with guidance；

var recrive,guid:L_radar；

colset L_incept=with fashe2；

var assign2,fire2,effect2:L_incept；

colset L_eval=with success2|fail2；

var waitfed2,eval2:L_eval；

圖2的CPN仿真模型如圖3所示。有來襲目標(biāo)時，預(yù)警雷達發(fā)出預(yù)警信息，指控中心開始工作，進行目標(biāo)確認并將目標(biāo)指示信息下達，指示高低層攔截系統(tǒng)同時做好攔截準(zhǔn)備。然后高層反導(dǎo)系統(tǒng)進行目標(biāo)攔截，并判斷是否攔截成功，如果成功則返回預(yù)警雷達繼續(xù)監(jiān)視，如果失敗，則由低層攔截系統(tǒng)實施攔截，這時無論是否攔截成功都將攔截結(jié)果返回上級指控中心。

圖3 反導(dǎo)作戰(zhàn)CPN tools模型

4.3 CPN Tools仿真結(jié)果分析

運行圖3所示CPN Tools仿真模型，進入狀態(tài)空間并指定狀態(tài)空間報告保存的位置和報告文件的名稱。下面是自動生成的部分狀態(tài)空間報告。

CPN Tools state space report:

Statistics

State Space

Nodes: 12

Arcs: 14

Secs: 0

Status: Full

Scc Graph

Nodes: 1

Arcs: 0

Secs: 0

Boundedness Properties

Best Integer Bounds …

Best Upper Multi-set Bounds …

Best Lower Multi-set Bounds …

Home Properties

Home Markings All

Liveness Properties

Dead Markings None

Dead Transition Instances None

Live Transition Instances All

Fairness Properties

Impartial Transition Instances

New_Page′'t21 1…

Fair Transition Instances

New_Page′t62 1 …

Just Transition Instances None

Transition Instances with No Fairness None

報告中，Statistics列出的是有關(guān)出現(xiàn)圖強連接圖的基本信息，State Space下的Nodes，Arcs，Secs分別是節(jié)點(標(biāo)示)數(shù)、弧連接數(shù)、生成圖所用的時間，Status表明生成出現(xiàn)圖是完整的。Scc Graph列舉了強連接圖的節(jié)點數(shù)和弧連接數(shù)。Home Properties列舉了歸屬標(biāo)識“All”，表明模型具有家態(tài)。Liveness Properties下分別列出了死節(jié)點“None”、死變遷“None”、活變遷“All”，表明模型無死鎖、有活性。Fairness Properties下列出了公平性的內(nèi)容。

仿真分析表明，該反導(dǎo)概念模型的CPN模型具有可達性、家態(tài)、有界性、無死鎖性和公平性等性質(zhì)，可以認為反導(dǎo)作戰(zhàn)概念模型是正確的。對于CMMS動態(tài)行為一致性的校驗，可采用對比的方法，將UML時序圖以及活動圖映射為CPN模型進行仿真，分析其邏輯和控制流程，驗證不同描述形式在表現(xiàn)動態(tài)行為上的吻合性，從而全面評估概念模型。

5 結(jié)束語

動態(tài)行為的驗證是任務(wù)空間概念模型校驗的重點和難點，對提高作戰(zhàn)模擬系統(tǒng)的可信性和可重用性都有著重要意義。論文以基于UML的反導(dǎo)作戰(zhàn)概念模型動態(tài)行為驗證的例子說明CPN以及用CPN Tools進行動態(tài)行為校驗的過程和方法。作為一種高級Petri網(wǎng)，CPN的圖形化表示簡單直觀，邏輯上運用類似“情況一處置”、“信息一處理”等的關(guān)系構(gòu)成的網(wǎng)絡(luò)便于進行計算機仿真，因此CPN在對缺乏準(zhǔn)確語義、難以進行語義分析和驗證的概念模型的分析校驗方面具有獨到的優(yōu)勢，通過計算機運行仿真工具，可以彌補人為的定性分析的不足，減少了專家主觀意識的影響，提高校驗結(jié)果的可信性。論文的研究為任務(wù)空間概念模型動態(tài)行為驗證提供了有益的探索和思考。

參 考 文 獻

[1] 王杏林，曹曉東.概念建模[M].北京：國防工業(yè)出版社，2007.(Wang Xinglin, Cao Xiaodong.Conceptual Modeling[M].BeiJing: National Defence Industry Press,2007.)

[2] Wagenhals L W，Harder S，Levis A H.Synthesizing Executable Models of Object Oriented Architectures[C].Workshop on Formal Methods Applied to Defense Systems，Adelaide，Australia，2002.

[3] 葉麗君.基于UML描述的概念模型校驗技術(shù)研究[D].鄭州：解放軍信息工程大學(xué)碩士學(xué)位論文，2008.(Ye Lijun.Research on the V&V technology of the conceptual model described by UML[D].Zheng Zhou: The PLA university of information engineering master's degree thesis,2008.)

[4] 鄢波，桑軍，向宏，胡海波.軟件體系結(jié)構(gòu)獲取過程的形式化描述方法比較[J].計算機工程，2009，35(21)：29-32.(Yan Bo, Sang Jun, Xiang Hong, Hu Haibo.Comparison of formal desecription methods for procedure of software architecture acquisition [J].Computer Engineering, 2009, 35(21):29-32.)

[5] 汪紅兵，徐安軍，姚琳，田乃媛.基于CPN煉鋼連鑄制造流程的建模與最優(yōu)調(diào)度求解[J].北京科技大學(xué)學(xué)報，2010，32(7)：938-945.(Wang Hongbing, Xu Anjun, Yao Lin, Tian Naiyuan.Modeling of steelmakeing continue-casting manufacturing flow using colored petri nets and solution of optimized scheduling[J].Journal of University of Sinence and Technology Bei Jing, 2010，32(7)：938-945.)

[6] Jensen K， Kristiansen L M， Wells L.Colored Petri Nets and CPN tools for modeling and validation of concurrent systems[J].International Journal on Software Tools For Technology Transfer，2007，9: 213.

[7] 曲長征，張柳，于永利，梁偉杰.基于ExSpect領(lǐng)域模型庫的裝備維修機構(gòu)仿真環(huán)境構(gòu)建[J].系統(tǒng)仿真學(xué)報，2009，21(9)：2772-2775.(Qu Changzheng, Zhang Liu, Yu Yongli, Liang Weijie.Development of maintenance organization modeling and simulation environment based on exspect domain library[J].Journal of System Simulation, 2009，21(9)：2772-2775.)

[8] Claude Girault，Rudiger Valk.Petri Nets for systems Engineering A Guide to Modeling ，Verification，And Applications[J].Publishing House of Electronics Industry，2005.

[9] 謝曉東.電子商務(wù)網(wǎng)絡(luò)協(xié)議的形式化分析理論與應(yīng)用[M].北京：科學(xué)出版社，2008.(Xie Xiaodong.The Electronic Commerce Network Protocol Formal Analysis Theory and Application[M].Bei Jing: Press of Science, 2008.)

[10] 李榮常，程建，鄭連清.空天一體信息作戰(zhàn)[M] .北京：軍事科學(xué)出版社，2003: 124.(Li Rongchang, Cheng Jian, Zheng Lianqing.Information warfare on the Integration of Space and Sky [M].Bei Jing：Press of Military Science ，2003.124.)