军事信息系统需求模型一致性检验方法*

禹明刚，权冀川，董经纬

（陆军工程大学指挥控制工程学院，南京 210007）

0 引言

军事信息系统从建设周期上可以划分为：项目规划、总体设计、分系统设计、系统实现4 个环节，其中需求分析是总体设计中最为关键的一环［1］。目前，军事信息系统的总体需求分析主要采用基于体系结构框架的分析方法，通过体系结构框架来严格规范需求描述，引导军事信息系统需求的获取和分析［2-3］。军事信息系统在需求分析阶段的主要分析产品是需求模型，需求模型的正确与否关系着整个系统建设的质量与成败。由于军事信息系统体系结构框架仅给出了抽象的、指导性的建模概念和原则，缺少形式化建模语义，因此，建立的需求模型往往存在建模语义不统一、描述不精确、违反领域规则等问题，对需求模型的分析与验证提出了挑战。

军事信息系统领域的需求验证研究大部分都针对体系结构的一致性验证展开。体系结构的一致性验证是指分析体系结构设计结果，判断不同视图、产品间对相同对象的描述是否存在语义上的矛盾和冲突，以及是否满足特定的领域规则约束。比较有代表性的方法包括：基于Petri 网模型的需求验证方法［4］、基于自动机理论的UML 活动图的业务模型检验方法［5］和基于KAOS 的需求分析方法［6］。

Petri 网能够显式描述系统的状态和事件，在描述离散事件动态系统方面具有较强的模型分析能力，但基于Petri 网模型的军事信息系统需求验证方法存在以下不足：1）模型转换为Petri 网后产生了大量库所和变迁，得到的Petri 网模型可读性差，易产生状态空间爆炸问题；2）在模型形式化到Petri网模型之前，对模型的描述作了某些约束，使得到的Petri 网模型与系统模型在原有语义上并不完全一致。

基于自动机理论的UML 活动图的业务模型检验方法在UML 活动图LTS 语义基础上，详细描述从UML 活动图生成LTS 的算法，然后将系统性质用线性时序逻辑（Linear Temporal Logic，LTL）表示并转换为相应的性质自动机，最终用基于自动机理论的模型检验方法，实现UML 活动图模型的自动检验，但该方法存在以下不足：1）UML 适用于软件工程领域而在军事特定领域适用性较差；2）由于系统性质，用线性时序逻辑表示，随着系统复杂度增加容易产生状态空间爆炸问题；3）该方法只能验证系统的行为逻辑，难以验证系统在概念设计上的一致性。

KAOS 是一种面向目标的需求获取、分析方法，通过目标分解和操作化实现需求的精化和规约，基于KAOS 的需求分析方法提供了一种基于时序逻辑和人工智能优化技术的形式化框架，可以给出需求中关于目标、状态等元素的一致性和严格的定义，但KAOS 方法在军事信息系统体系结构框架中的适用性较差，缺少体系结构框架建模元素，导致需求描述能力不足。

本研究通过比较现有需求分析验证方法，提出了基于本体和描述逻辑的军事信息系统需求模型一致性检验技术。方法构建了军事信息系统需求概念本体，为描述和理解军事信息系统的业务领域概念和系统开发需求提供了语义一致、含义明确的公共术语；提出了军事信息系统三层概念建模框架，利用扩展的UML Profile 构建多个视图，从不同刻面全面系统地描述了军事信息系统的应用需求；引入了基于描述逻辑SHOIN（D）［7］的军事信息系统需求模型一致性验证技术，描述逻辑本身是可判定的，该技术利用定理证明方式对军事信息系统需求模型进行严格的一致性验证。本方法为军事信息系统需求分析和验证提供了新的思路，与传统方法相比，本方法具有自动化程度高、知识复用能力强、推理效率高等特点。

1 军事信息系统需求模型一致性检验方法总体架构

军事信息系统需求模型一致性检验方法由构建军事信息系统需求概念本体、定义模型视图、进行模型－本体转换等共6 个步骤组成，如图1 所示。

图1 军事信息系统需求模型一致性检验方法总体架构

首先，定义军事信息系统需求描述中最基本的概念以及概念间的关系，构成军事信息系统需求概念本体，本体的目的在于规范和约束需求模型的建立，同时可以作为需求模型一致性检查的知识库；然后，通过UML Profile 扩展机制，构建军事信息系统特定领域需求建模语言，为需求描述提供语法、语义约束；利用领域建模语言定义模型视图，构建需求模型，需求模型是一致性检验的对象，是描述逻辑系统的输入；将构建的需求模型转换为SHION（D）本体，将半形式化的UML 语言转换为基于描述逻辑的形式化语言，为下一步推理验证奠定基础；将转换得到的需求本体导入推理引擎，同时导入一致性检验规则，启动推理引擎，推理引擎向需求分析人员返回模型一致性检验结果；最后，针对检验结果，需求分析人员对需求模型进行调整和修正，并开始新一轮的一致性验证，直到得出一致性结论。

下文将围绕框架涉及的军事信息系统需求概念本体、基于UML 的军事信息系统需求建模方法和基于描述逻辑的需求模型推理验证技术3 个关键部分展开论述。

2 军事信息系统需求概念本体

军事信息系统需求概念本体通过总结美军DoDAF2.0［8］和英军MODAF1.0［9］的主要思想，并参照我军信息系统应用领域业务规范术语以及工程项目术语规范要求，抽取了军事信息系统体系结构中最为基本的概念以及概念间的关系。

军事信息系统需求概念本体定义为三元组：

Requirement_Ontology=＜Concepts，Relations，Rules ＞。其中，Concepts 是本体概念集合，包含了军事信息系统领域所有相关概念；Relations 是元本体概念之间关系的集合，包含了本体概念之间所有的关系；Rules 是本体的规则集合，定义了本体概念与本体关系之间必须遵守的永真断言，是一组约束军事信息系统需求模型的规则，它描述了通用领域知识和特定领域规则。军事信息系统需求概念本体详见附录。

军事信息系统需求概念本体是一致性检验技术的基础和核心，是军事信息系统需求模型的抽象，其目的在于引导和规范需求模型的建立。

3 基于UML 的军事信息系统需求建模方法

虽然军事信息系统需求概念本体明确了军事信息系统领域内最为基本的概念、关系及规则，严格规范了领域相关概念的语法语义。但是，需求概念本体本身并没有领域特定的含义，在应用建模中不能准确地定义需求，因此，需要在特定领域概念化，即建立领域概念化模型。领域化模型是领域专家在概念本体框架下定义的领域特定概念及其关系，这些概念在特定领域中含义明确且普遍适用。

本研究提出如图2 所示的三层概念建模框架，框架分为3 个抽象层次，分别是元概念层、领域概念层和应用概念层。

元概念由军事信息系统需求概念本体中的概念、关系及规则组成，属于顶层概念，用于定义领域概念的基本概念。元概念层对应于MDA［10-11］元建模机制的M2 层。领域概念层的领域概念是特定领域中约定成俗的抽象概念，如“机动作战能力”（来源于需求概念本体中的“能力”）。领域概念层对应于MDA 元建模机制的M1 层。应用概念是用领域特定概念定义或语义约束的，用来描述某个具体应用的概念，如由“机动作战能力”实例化导出的具体应用概念“X 型装甲车作战能力”。应用概念层对应于MDA 元建模机制的M0 层。在概念建模的三层结构中，上层概念是对下层概念的抽象，下层概念是对上层概念的复用和实例化。

图2 概念建模的三层结构

军事信息系统需求建模过程分为3 个步骤［12-14］：1）严格遵守需求概念本体的语义规范，扩展UML Profile 构建军事信息系统领域建模语言。2）在需求概念本体的引导约束下，针对各个视图构建领域概念模型。3）需求分析人员通过与作为系统用户的各利益相关方进行交流，掌握其对系统的具体需求，针对具体作战想定通过复用和实例化领域概念模型构建需求模型，需求模型反映了系统用户的最终需求，是一致性检验的对象。

4 基于描述逻辑的军事信息系统需求模型一致性验证技术

需求模型与概念本体之间可能会存在语义上的一致性问题；与此同时在语用层面上，需求模型反映了特定领域的领域知识，模型中可能会存在违反现实领域知识或规则的一致性问题［15-18］。因此，需求模型中可能存在两大类一致性问题：

1）需求模型语义层面的一致性问题；

2）违反领域知识的一致性问题。又可分为：

*违反通用领域知识的一致性问题；

*违反特定领域规则的一致性问题。

军事信息系统需求模型基于半形式化语言UML 构建，因此，无法进行形式化推理验证，为了实现计算机对需求模型的自动检验，本研究提出将需求分析人员构建的军事信息系统需求模型转换为军事信息系统需求本体，然后借助计算机领域成熟的本体推理技术，实现对军事信息系统需求模型的自动检验分析。需求模型的一致性验证技术主要包括3 部分内容：需求模型的本体转换、需求模型的一致性规则定义和需求模型的一致性推理检验。

4.1 需求模型的本体转换

SHOIN（D）是目前广泛使用的描述逻辑子语言，它不仅继承了描述逻辑强大的知识表达能力，而且具备推理可判定性，业界还开发了支持SHOIN（D）系统自动推理的自动推理引擎。因此，本节采用SHOIN（D）作为需求模型中数据元素到描述逻辑本体知识库的转换桥梁。

本文定义的军事信息系统需求概念本体，以及在该概念本体引导和约束下构建的需求模型与OMG 组织的四层模型体系对应关系如下页图3 所示。根据这种对应关系，将军事信息系统需求概念本体形式化为本体知识库的Tbox，将需求模型形式化为本体知识库的Abox。

军事信息系统需求概念本体及需求模型的本体转换算法如下所示：

?

图3 SHOIN（D）本体与概念本体及需求模型映射

读取概念本体中的类，根据类名在Tbox 中创建同名概念，并明确该类与其他类的继承关系；读取概念本体中的关系，根据关系名在Tbox 中创建同名关系，并明确关系两端的基数约束；读取需求模型中的每个实例及关系，在Abox 中添加与Tbox 相应的实例与关系的声明。

4.2 需求模型的一致性规则定义

一致性检验规则是对需求模型进行检验和分析的依据，针对需求模型中可能存在的两大类一致性问题需要分别考虑一致性检验规则。

1）针对语义层面一致性问题，需求分析人员无需另外定义检验规则，Tableaux 算法本身推理机制可以针对本体逻辑一致性、概念的一致性、概念的包容关系、概念等价关系、隐含的不一致性等问题作出回应。

2）针对违反领域知识的一致性问题，需要分别对通用领域知识和特定领域规则定义一致性检验规则。

1）基于通用领域知识的一致性检验规则

通用领域知识一致性检验规则用于检查领域概念模型是否符合领域规范和常识性要求。该类规则主要来自于DoDAF2.0 提出的体系结构通用领域知识，大部分是对概念间基数的自由数量约束、相对数量约束、等量数量约束等。

2）基于特定领域业务规则的一致性检验规则

基于特定领域业务规则的一致性检验规则用于发现需求模型内存在的违反特定领域的业务规则。该类规则主要来自于具体作战业务的条令条例和规章制度等，从描述这些规则的语法结构上看可将其视为“IF ＜前提条件＞THEN ＜导致结果＞”的推理演绎规则。

另外，基于特定领域业务规则的一致性检验规则通常采用自然语言或类自然语言描述，因此，需要将该规则转换为可以被描述逻辑系统识别和理解的特定语言，即本文中采用的语义网规则描述语言（Semantic Web Rule Language，SWRL）［19］。领域业务规则的转换算法Construct RSWRL 如下：

?

前提和结论中的概念、概念属性、概念间关系都被转换为Horn 子句的前题和结果，通过逻辑连接符将Horn 子句的前题和结果分别组合为SWRL 的条件和推论。需要指出的是特定领域业务规则的内容和数量并无统一的标准规范，需求分析人员可以针对领域的业务特点定制特定领域业务规则，并可以在实际应用中由领域专家不断加以丰富和完善，随时添加到知识库中，因此，具备较强的灵活性。

4.3 需求模型的一致性推理检验

针对第1 类语义层面的一致性问题，在加载本体后，需求分析人员输入一致性查询指令“Pellet consistency-v xxx.owl”，推理引擎会自动执行基于Tableaux 的一致性推理算法，判断需求模型中存在的语义不一致性问题，并向用户返回推理结果。

针对第2 类违反领域知识的一致性问题，经推理引擎逻辑推理后，最终需要通过Abox 个体查询方式获得领域知识一致性验证结果。本研究针对两类领域知识一致性检验规则分别设计对应的SPARQL［20］查询语句，限制个体查询条件，从而获得需求分析人员关心的模型验证结果。

常用的SPARQL 语句结构如下所示：

需求分析人员用每条领域规则对应的SPARQL语句来查询违反领域知识一致性的个体，如果该规则的查询结果为空，表明需求模型中的数据元素满足该规则约束，如果该规则的查询结果不为空，则结果中的对象所代表的需求模型中的数据元素不满足该约束。当所有规则的查询结果都为空时，才表明需求模型中的数据元素满足所有的领域知识的约束，从而完成需求模型的一致性检验。

5 案例分析

某城市一体化防空作战指挥系统是一个典型的军事信息系统，主要用于保卫城市重要目标免遭巡航导弹、空地导弹等突袭，形成区域防空最后一道防线的作战指挥。需求分析人员在开发某城市防空一体化作战系统时，在军事信息系统概念本体引导下，建立领域概念模型，并通过实例化领域概念构建某城市的防空一体化作战系统需求模型。需求分析人员针对不同视图可以构建多个需求模型，从不同刻面描述该一体化防空作战指挥系统的军事需求。本案例为简化问题，节选了部分领域概念和应用需求概念，构建了该系统的需求模型，如图4所示。

借助于本文提出的军事信息系统概念本体及需求模型的本体转换算法将概念本体及需求模型转换为需求本体。限于篇幅，下页表1 仅列出部分重要公理和事实断言。

图4 X 防空一体化作战系统需求模型

5.1 需求模型语义层面的一致性检验问题

假设在构建一体化防空作战指挥系统的需求模型中，由于需求分析人员的失误，在“快速摧毁空袭目标DDT20”与“X 防空一体化作战系统防空作战能力x-SADC”之间错误地添加了“指导活动DEPA”关系，而在需求概念本体的语义约束中，“指导活动DEPA”关系只存在于“预期效果Desired Effect”和“活动Activity”之间，因此，导致语义层面的不一致性。

以上不一致性问题采用Pellet 1.5.0 本体推理引擎，加载本体文件“防空案例.owl”，输入查询命令“Pellet consistency-v 防空案例.owl”，推理引擎自动返回如图5 所示的推理结果。

推理界面中显示：

图5 X 防空一体化作战系统需求模型一致性验证

结果说明“指导活动”DEPA 关系本来应该存在于实例DDT20 和Activity 的某个实例之间，而在构建的需求模型里把DEPA 关系赋予了DDT20 和x-SADC，所以x-SADC 被错误地强制作为Activity的实例。

5.2 领域知识的一致性检验问题

违反领域知识的一致性问题又可分为违反通用领域知识的一致性问题和违反特定领域规则的一致性问题。

表1 X 防空一体化作战系统需求本体

5.2.1 违反通用领域知识的一致性问题

通用领域规则有很多，例如：“目标至少有一个支持其实现的能力”、“战略目标要分解成一个以上的使命组合”、“能力必须要有作战活动来体现”、“作战活动必须拥有一个执行者”等，本案例以“作战活动必须拥有一个执行者”为例说明通用领域知识的一致性检验过程。此类问题通过对Abox 个体的一致性查询来发现需求模型的不一致，查询需求模型中不存在执行者的活动，对应的SPARQL 查询语句是：

向推理引擎输入上述查询规则，引擎返回如图6 所示的推理结果。

结果显示，在需求模型中存在违反此规则的个体“x-CADA”，即“X 空域防空活动”没有执行者。下一步，需求分析人员需要对构建的需求模型进行修改，针对作战想定，在“X 空域防空活动”与某特定执行者之间添加代表执行关系的需求线。

图6 X 防空一体化作战系统需求模型通用领域知识一致性验证

5.2.2 违反特定领域规则的一致性问题特定领域规则与需求的应用背景相关。可以根据该领域现有规章制度（如作战条令条例等）或在领域知识框架的基础上新定义一些领域推理检验规则。

在防空作战条令的导弹发射业务章程中规定：在导弹打击任务中，任何导弹发射活动的执行必须有导弹发射指令作为前提条件。即如果部队有导弹打击任务并且导弹已经发射，那么一定存在一条导弹发射指令。根据发明内容中设计的SWRL 规则转换算法，该条特定领域规则对应的SWRL 语句为：

将上述规则导入公理集Tbox，需求分析人员采用Abox 个体查询，查询无导弹发射指令约束的活动，对应的SPARQL 查询语句是：

引擎返回如图7 所示的推理结果。

图7 X 防空一体化作战系统需求模型特定领域规则一致性验证

结果显示，在需求模型中存在违反上述规则的个体“x-SDMLA”和“y-LDMLA”，即“x 型近程导弹发射活动”和“y 型远程导弹发射活动”均无导弹发射指令的约束。针对该不一致情况，需求分析人员需对构建的需求模型进行进一步的活动分析，在上述两项导弹发射活动的约束中添加相应的发射指令。

6 结论

本文提出一种军事信息系统需求模型一致性检验技术，可以有效检验需求分析人员所构建的需求模型的语义是否正确，内容是否全面如实地反映用户要求，进而为系统后续建设提供参考和决策支持。与传统方法比，本方法具备以下特点：1）自动化程度高。军事信息系统需求模型一致性检验技术基于成熟的Tableaux 算法，拥有Pellet、Protege 等多种推理引擎和工具作为支撑，保证了较高的自动化程度；2）知识复用能力强。Petri 网、线性时序逻辑等需求分析验证方法均针对具体个例建模，不具备复用性。本文提出的需求概念本体及一致性检验规则在构建不同的需求模型时均可重复利用，具备较强的知识复用性；3）推理效率高。随着军事信息系统复杂性增加，整个系统产生的状态量呈指数增长，线性时序逻辑等作为以穷尽搜索为基础的模型检测技术，状态爆炸问题一直是制约其发展的瓶颈。基于描述逻辑的军事信息系统需求模型一致性检验方法既可以验证有穷状态系统，又可使用归纳的方法处理无限状态问题，很好地规避了状态爆炸问题。