基于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.)