基于UML的任務空間概念模型動態行為驗證研究*

高江林 吳曉燕

空軍工程大學導彈學院，陜西三原 713800

任務空間概念模型(Conceptual Models of the Mission Space，CMMS)以一種獨立于仿真實現的方式[1]，描述了軍事行動相關的過程、實體、關系，成為作戰模擬系統開發的共同起點和權威標準，在領域專家和開發人員之間扮演著橋梁和溝通作用。高質量的概念模型需要經過反復的校驗，它是仿真可信度的基礎。由于任務空間概念模型靜態部分的內容比較容易理解和檢查，而動態部分的邏輯性、合理性等內容則由于行為的復雜性、缺乏有效的驗證手段成為概念模型校驗的難點和重點。

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

1 CMMS動態行為驗證基礎

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

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

圖1 基于CPN的動態行為驗證過程

2 CMMS動態行為驗證內容

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

在驗證正確性時，要根據目的選擇模型所需滿足的性質，當Petri網模型表現出一組所需要的性質時，就認為概念模型是正確的。Petri網有許多重要性質，下面給出對概念模型正確性有較大影響的Petri網的性質描述[8]：

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

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

3)無死鎖性：不存在死標識，意味著系統中不會發生全局死鎖;

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

5)家態：存在一個從任何其他標識都可以到達的標識，指出系統可以重新初始化其自身;

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

3 CPN Tools仿真

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

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

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

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

4 基于UML的反導作戰概念模型動態行為驗證

4.1 反導作戰概念模型UML描述

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

圖2 末段高低兩層反導作戰時序圖

其中，信息流數據分別為：

info(1)：BM發射預警信息，目標彈道的估算數據。

info(2)：BM發射預警信息，目標指示信息。

info(3)：實時目標信息，目標識別信息，攔截導彈發射所需數據等。

info(4)：目標初步指示信息，下達作戰命令。

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

info(6)：目標指示信息，制導雷達狀態指令，能量分配控制。

info(7)：目標識別信息，導彈發射裝訂參數，制導方式轉換指令。

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

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

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

feedback(1)：目標指示信息，預警雷達狀態信息，能量分配控制。

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

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

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

4.2 CPN 模型

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

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所示。有來襲目標時，預警雷達發出預警信息，指控中心開始工作，進行目標確認并將目標指示信息下達，指示高低層攔截系統同時做好攔截準備。然后高層反導系統進行目標攔截，并判斷是否攔截成功，如果成功則返回預警雷達繼續監視，如果失敗，則由低層攔截系統實施攔截，這時無論是否攔截成功都將攔截結果返回上級指控中心。

圖3 反導作戰CPN tools模型

4.3 CPN Tools仿真結果分析

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

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列出的是有關出現圖強連接圖的基本信息，State Space下的Nodes，Arcs，Secs分別是節點(標示)數、弧連接數、生成圖所用的時間，Status表明生成出現圖是完整的。Scc Graph列舉了強連接圖的節點數和弧連接數。Home Properties列舉了歸屬標識“All”，表明模型具有家態。Liveness Properties下分別列出了死節點“None”、死變遷“None”、活變遷“All”，表明模型無死鎖、有活性。Fairness Properties下列出了公平性的內容。

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

5 結束語

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

參 考 文 獻

[1] 王杏林，曹曉東.概念建模[M].北京：國防工業出版社，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描述的概念模型校驗技術研究[D].鄭州：解放軍信息工程大學碩士學位論文，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] 鄢波，桑軍，向宏，胡海波.軟件體系結構獲取過程的形式化描述方法比較[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煉鋼連鑄制造流程的建模與最優調度求解[J].北京科技大學學報，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領域模型庫的裝備維修機構仿真環境構建[J].系統仿真學報，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] 謝曉東.電子商務網絡協議的形式化分析理論與應用[M].北京：科學出版社，2008.(Xie Xiaodong.The Electronic Commerce Network Protocol Formal Analysis Theory and Application[M].Bei Jing: Press of Science, 2008.)

[10] 李榮常，程建，鄭連清.空天一體信息作戰[M] .北京：軍事科學出版社，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.)