高江林 吴晓燕

空军工程大学导弹学院，陕西三原 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网建立概念模型的可执行模型，并进行仿真验证、性能评价变得可行而实用。……