軍事信息系統(tǒng)需求模型一致性檢驗(yàn)方法*

禹明剛，權(quán)冀川，董經(jīng)緯

（陸軍工程大學(xué)指揮控制工程學(xué)院，南京 210007）

0 引言

軍事信息系統(tǒng)從建設(shè)周期上可以劃分為：項(xiàng)目規(guī)劃、總體設(shè)計(jì)、分系統(tǒng)設(shè)計(jì)、系統(tǒng)實(shí)現(xiàn)4 個(gè)環(huán)節(jié)，其中需求分析是總體設(shè)計(jì)中最為關(guān)鍵的一環(huán)［1］。目前，軍事信息系統(tǒng)的總體需求分析主要采用基于體系結(jié)構(gòu)框架的分析方法，通過體系結(jié)構(gòu)框架來嚴(yán)格規(guī)范需求描述，引導(dǎo)軍事信息系統(tǒng)需求的獲取和分析［2-3］。軍事信息系統(tǒng)在需求分析階段的主要分析產(chǎn)品是需求模型，需求模型的正確與否關(guān)系著整個(gè)系統(tǒng)建設(shè)的質(zhì)量與成敗。由于軍事信息系統(tǒng)體系結(jié)構(gòu)框架僅給出了抽象的、指導(dǎo)性的建模概念和原則，缺少形式化建模語義，因此，建立的需求模型往往存在建模語義不統(tǒng)一、描述不精確、違反領(lǐng)域規(guī)則等問題，對(duì)需求模型的分析與驗(yàn)證提出了挑戰(zhàn)。

軍事信息系統(tǒng)領(lǐng)域的需求驗(yàn)證研究大部分都針對(duì)體系結(jié)構(gòu)的一致性驗(yàn)證展開。體系結(jié)構(gòu)的一致性驗(yàn)證是指分析體系結(jié)構(gòu)設(shè)計(jì)結(jié)果，判斷不同視圖、產(chǎn)品間對(duì)相同對(duì)象的描述是否存在語義上的矛盾和沖突，以及是否滿足特定的領(lǐng)域規(guī)則約束。比較有代表性的方法包括：基于Petri 網(wǎng)模型的需求驗(yàn)證方法［4］、基于自動(dòng)機(jī)理論的UML 活動(dòng)圖的業(yè)務(wù)模型檢驗(yàn)方法［5］和基于KAOS 的需求分析方法［6］。

Petri 網(wǎng)能夠顯式描述系統(tǒng)的狀態(tài)和事件，在描述離散事件動(dòng)態(tài)系統(tǒng)方面具有較強(qiáng)的模型分析能力，但基于Petri 網(wǎng)模型的軍事信息系統(tǒng)需求驗(yàn)證方法存在以下不足：1）模型轉(zhuǎn)換為Petri 網(wǎng)后產(chǎn)生了大量庫所和變遷，得到的Petri 網(wǎng)模型可讀性差，易產(chǎn)生狀態(tài)空間爆炸問題；2）在模型形式化到Petri網(wǎng)模型之前，對(duì)模型的描述作了某些約束，使得到的Petri 網(wǎng)模型與系統(tǒng)模型在原有語義上并不完全一致。

基于自動(dòng)機(jī)理論的UML 活動(dòng)圖的業(yè)務(wù)模型檢驗(yàn)方法在UML 活動(dòng)圖LTS 語義基礎(chǔ)上，詳細(xì)描述從UML 活動(dòng)圖生成LTS 的算法，然后將系統(tǒng)性質(zhì)用線性時(shí)序邏輯（Linear Temporal Logic，LTL）表示并轉(zhuǎn)換為相應(yīng)的性質(zhì)自動(dòng)機(jī)，最終用基于自動(dòng)機(jī)理論的模型檢驗(yàn)方法，實(shí)現(xiàn)UML 活動(dòng)圖模型的自動(dòng)檢驗(yàn)，但該方法存在以下不足：1）UML 適用于軟件工程領(lǐng)域而在軍事特定領(lǐng)域適用性較差；2）由于系統(tǒng)性質(zhì)，用線性時(shí)序邏輯表示，隨著系統(tǒng)復(fù)雜度增加容易產(chǎn)生狀態(tài)空間爆炸問題；3）該方法只能驗(yàn)證系統(tǒng)的行為邏輯，難以驗(yàn)證系統(tǒng)在概念設(shè)計(jì)上的一致性。

KAOS 是一種面向目標(biāo)的需求獲取、分析方法，通過目標(biāo)分解和操作化實(shí)現(xiàn)需求的精化和規(guī)約，基于KAOS 的需求分析方法提供了一種基于時(shí)序邏輯和人工智能優(yōu)化技術(shù)的形式化框架，可以給出需求中關(guān)于目標(biāo)、狀態(tài)等元素的一致性和嚴(yán)格的定義，但KAOS 方法在軍事信息系統(tǒng)體系結(jié)構(gòu)框架中的適用性較差，缺少體系結(jié)構(gòu)框架建模元素，導(dǎo)致需求描述能力不足。

本研究通過比較現(xiàn)有需求分析驗(yàn)證方法，提出了基于本體和描述邏輯的軍事信息系統(tǒng)需求模型一致性檢驗(yàn)技術(shù)。方法構(gòu)建了軍事信息系統(tǒng)需求概念本體，為描述和理解軍事信息系統(tǒng)的業(yè)務(wù)領(lǐng)域概念和系統(tǒng)開發(fā)需求提供了語義一致、含義明確的公共術(shù)語；提出了軍事信息系統(tǒng)三層概念建?？蚣埽脭U(kuò)展的UML Profile 構(gòu)建多個(gè)視圖，從不同刻面全面系統(tǒng)地描述了軍事信息系統(tǒng)的應(yīng)用需求；引入了基于描述邏輯SHOIN（D）［7］的軍事信息系統(tǒng)需求模型一致性驗(yàn)證技術(shù)，描述邏輯本身是可判定的，該技術(shù)利用定理證明方式對(duì)軍事信息系統(tǒng)需求模型進(jìn)行嚴(yán)格的一致性驗(yàn)證。本方法為軍事信息系統(tǒng)需求分析和驗(yàn)證提供了新的思路，與傳統(tǒng)方法相比，本方法具有自動(dòng)化程度高、知識(shí)復(fù)用能力強(qiáng)、推理效率高等特點(diǎn)。

1 軍事信息系統(tǒng)需求模型一致性檢驗(yàn)方法總體架構(gòu)

軍事信息系統(tǒng)需求模型一致性檢驗(yàn)方法由構(gòu)建軍事信息系統(tǒng)需求概念本體、定義模型視圖、進(jìn)行模型－本體轉(zhuǎn)換等共6 個(gè)步驟組成，如圖1 所示。

圖1 軍事信息系統(tǒng)需求模型一致性檢驗(yàn)方法總體架構(gòu)

首先，定義軍事信息系統(tǒng)需求描述中最基本的概念以及概念間的關(guān)系，構(gòu)成軍事信息系統(tǒng)需求概念本體，本體的目的在于規(guī)范和約束需求模型的建立，同時(shí)可以作為需求模型一致性檢查的知識(shí)庫；然后，通過UML Profile 擴(kuò)展機(jī)制，構(gòu)建軍事信息系統(tǒng)特定領(lǐng)域需求建模語言，為需求描述提供語法、語義約束；利用領(lǐng)域建模語言定義模型視圖，構(gòu)建需求模型，需求模型是一致性檢驗(yàn)的對(duì)象，是描述邏輯系統(tǒng)的輸入；將構(gòu)建的需求模型轉(zhuǎn)換為SHION（D）本體，將半形式化的UML 語言轉(zhuǎn)換為基于描述邏輯的形式化語言，為下一步推理驗(yàn)證奠定基礎(chǔ)；將轉(zhuǎn)換得到的需求本體導(dǎo)入推理引擎，同時(shí)導(dǎo)入一致性檢驗(yàn)規(guī)則，啟動(dòng)推理引擎，推理引擎向需求分析人員返回模型一致性檢驗(yàn)結(jié)果；最后，針對(duì)檢驗(yàn)結(jié)果，需求分析人員對(duì)需求模型進(jìn)行調(diào)整和修正，并開始新一輪的一致性驗(yàn)證，直到得出一致性結(jié)論。

下文將圍繞框架涉及的軍事信息系統(tǒng)需求概念本體、基于UML 的軍事信息系統(tǒng)需求建模方法和基于描述邏輯的需求模型推理驗(yàn)證技術(shù)3 個(gè)關(guān)鍵部分展開論述。

2 軍事信息系統(tǒng)需求概念本體

軍事信息系統(tǒng)需求概念本體通過總結(jié)美軍DoDAF2.0［8］和英軍MODAF1.0［9］的主要思想，并參照我軍信息系統(tǒng)應(yīng)用領(lǐng)域業(yè)務(wù)規(guī)范術(shù)語以及工程項(xiàng)目術(shù)語規(guī)范要求，抽取了軍事信息系統(tǒng)體系結(jié)構(gòu)中最為基本的概念以及概念間的關(guān)系。

軍事信息系統(tǒng)需求概念本體定義為三元組：

Requirement_Ontology=＜Concepts，Relations，Rules ＞。其中，Concepts 是本體概念集合，包含了軍事信息系統(tǒng)領(lǐng)域所有相關(guān)概念；Relations 是元本體概念之間關(guān)系的集合，包含了本體概念之間所有的關(guān)系；Rules 是本體的規(guī)則集合，定義了本體概念與本體關(guān)系之間必須遵守的永真斷言，是一組約束軍事信息系統(tǒng)需求模型的規(guī)則，它描述了通用領(lǐng)域知識(shí)和特定領(lǐng)域規(guī)則。軍事信息系統(tǒng)需求概念本體詳見附錄。

軍事信息系統(tǒng)需求概念本體是一致性檢驗(yàn)技術(shù)的基礎(chǔ)和核心，是軍事信息系統(tǒng)需求模型的抽象，其目的在于引導(dǎo)和規(guī)范需求模型的建立。

3 基于UML 的軍事信息系統(tǒng)需求建模方法

雖然軍事信息系統(tǒng)需求概念本體明確了軍事信息系統(tǒng)領(lǐng)域內(nèi)最為基本的概念、關(guān)系及規(guī)則，嚴(yán)格規(guī)范了領(lǐng)域相關(guān)概念的語法語義。但是，需求概念本體本身并沒有領(lǐng)域特定的含義，在應(yīng)用建模中不能準(zhǔn)確地定義需求，因此，需要在特定領(lǐng)域概念化，即建立領(lǐng)域概念化模型。領(lǐng)域化模型是領(lǐng)域?qū)＜以诟拍畋倔w框架下定義的領(lǐng)域特定概念及其關(guān)系，這些概念在特定領(lǐng)域中含義明確且普遍適用。

本研究提出如圖2 所示的三層概念建?？蚣埽蚣芊譃? 個(gè)抽象層次，分別是元概念層、領(lǐng)域概念層和應(yīng)用概念層。

元概念由軍事信息系統(tǒng)需求概念本體中的概念、關(guān)系及規(guī)則組成，屬于頂層概念，用于定義領(lǐng)域概念的基本概念。元概念層對(duì)應(yīng)于MDA［10-11］元建模機(jī)制的M2 層。領(lǐng)域概念層的領(lǐng)域概念是特定領(lǐng)域中約定成俗的抽象概念，如“機(jī)動(dòng)作戰(zhàn)能力”（來源于需求概念本體中的“能力”）。領(lǐng)域概念層對(duì)應(yīng)于MDA 元建模機(jī)制的M1 層。應(yīng)用概念是用領(lǐng)域特定概念定義或語義約束的，用來描述某個(gè)具體應(yīng)用的概念，如由“機(jī)動(dòng)作戰(zhàn)能力”實(shí)例化導(dǎo)出的具體應(yīng)用概念“X 型裝甲車作戰(zhàn)能力”。應(yīng)用概念層對(duì)應(yīng)于MDA 元建模機(jī)制的M0 層。在概念建模的三層結(jié)構(gòu)中，上層概念是對(duì)下層概念的抽象，下層概念是對(duì)上層概念的復(fù)用和實(shí)例化。

圖2 概念建模的三層結(jié)構(gòu)

軍事信息系統(tǒng)需求建模過程分為3 個(gè)步驟［12-14］：1）嚴(yán)格遵守需求概念本體的語義規(guī)范，擴(kuò)展UML Profile 構(gòu)建軍事信息系統(tǒng)領(lǐng)域建模語言。2）在需求概念本體的引導(dǎo)約束下，針對(duì)各個(gè)視圖構(gòu)建領(lǐng)域概念模型。3）需求分析人員通過與作為系統(tǒng)用戶的各利益相關(guān)方進(jìn)行交流，掌握其對(duì)系統(tǒng)的具體需求，針對(duì)具體作戰(zhàn)想定通過復(fù)用和實(shí)例化領(lǐng)域概念模型構(gòu)建需求模型，需求模型反映了系統(tǒng)用戶的最終需求，是一致性檢驗(yàn)的對(duì)象。

4 基于描述邏輯的軍事信息系統(tǒng)需求模型一致性驗(yàn)證技術(shù)

需求模型與概念本體之間可能會(huì)存在語義上的一致性問題；與此同時(shí)在語用層面上，需求模型反映了特定領(lǐng)域的領(lǐng)域知識(shí)，模型中可能會(huì)存在違反現(xiàn)實(shí)領(lǐng)域知識(shí)或規(guī)則的一致性問題［15-18］。因此，需求模型中可能存在兩大類一致性問題：

1）需求模型語義層面的一致性問題；

2）違反領(lǐng)域知識(shí)的一致性問題。又可分為：

*違反通用領(lǐng)域知識(shí)的一致性問題；

*違反特定領(lǐng)域規(guī)則的一致性問題。

軍事信息系統(tǒng)需求模型基于半形式化語言UML 構(gòu)建，因此，無法進(jìn)行形式化推理驗(yàn)證，為了實(shí)現(xiàn)計(jì)算機(jī)對(duì)需求模型的自動(dòng)檢驗(yàn)，本研究提出將需求分析人員構(gòu)建的軍事信息系統(tǒng)需求模型轉(zhuǎn)換為軍事信息系統(tǒng)需求本體，然后借助計(jì)算機(jī)領(lǐng)域成熟的本體推理技術(shù)，實(shí)現(xiàn)對(duì)軍事信息系統(tǒng)需求模型的自動(dòng)檢驗(yàn)分析。需求模型的一致性驗(yàn)證技術(shù)主要包括3 部分內(nèi)容：需求模型的本體轉(zhuǎn)換、需求模型的一致性規(guī)則定義和需求模型的一致性推理檢驗(yàn)。

4.1 需求模型的本體轉(zhuǎn)換

SHOIN（D）是目前廣泛使用的描述邏輯子語言，它不僅繼承了描述邏輯強(qiáng)大的知識(shí)表達(dá)能力，而且具備推理可判定性，業(yè)界還開發(fā)了支持SHOIN（D）系統(tǒng)自動(dòng)推理的自動(dòng)推理引擎。因此，本節(jié)采用SHOIN（D）作為需求模型中數(shù)據(jù)元素到描述邏輯本體知識(shí)庫的轉(zhuǎn)換橋梁。

本文定義的軍事信息系統(tǒng)需求概念本體，以及在該概念本體引導(dǎo)和約束下構(gòu)建的需求模型與OMG 組織的四層模型體系對(duì)應(yīng)關(guān)系如下頁圖3 所示。根據(jù)這種對(duì)應(yīng)關(guān)系，將軍事信息系統(tǒng)需求概念本體形式化為本體知識(shí)庫的Tbox，將需求模型形式化為本體知識(shí)庫的Abox。

軍事信息系統(tǒng)需求概念本體及需求模型的本體轉(zhuǎn)換算法如下所示：

?

圖3 SHOIN（D）本體與概念本體及需求模型映射

讀取概念本體中的類，根據(jù)類名在Tbox 中創(chuàng)建同名概念，并明確該類與其他類的繼承關(guān)系；讀取概念本體中的關(guān)系，根據(jù)關(guān)系名在Tbox 中創(chuàng)建同名關(guān)系，并明確關(guān)系兩端的基數(shù)約束；讀取需求模型中的每個(gè)實(shí)例及關(guān)系，在Abox 中添加與Tbox 相應(yīng)的實(shí)例與關(guān)系的聲明。

4.2 需求模型的一致性規(guī)則定義

一致性檢驗(yàn)規(guī)則是對(duì)需求模型進(jìn)行檢驗(yàn)和分析的依據(jù)，針對(duì)需求模型中可能存在的兩大類一致性問題需要分別考慮一致性檢驗(yàn)規(guī)則。

1）針對(duì)語義層面一致性問題，需求分析人員無需另外定義檢驗(yàn)規(guī)則，Tableaux 算法本身推理機(jī)制可以針對(duì)本體邏輯一致性、概念的一致性、概念的包容關(guān)系、概念等價(jià)關(guān)系、隱含的不一致性等問題作出回應(yīng)。

2）針對(duì)違反領(lǐng)域知識(shí)的一致性問題，需要分別對(duì)通用領(lǐng)域知識(shí)和特定領(lǐng)域規(guī)則定義一致性檢驗(yàn)規(guī)則。

1）基于通用領(lǐng)域知識(shí)的一致性檢驗(yàn)規(guī)則

通用領(lǐng)域知識(shí)一致性檢驗(yàn)規(guī)則用于檢查領(lǐng)域概念模型是否符合領(lǐng)域規(guī)范和常識(shí)性要求。該類規(guī)則主要來自于DoDAF2.0 提出的體系結(jié)構(gòu)通用領(lǐng)域知識(shí)，大部分是對(duì)概念間基數(shù)的自由數(shù)量約束、相對(duì)數(shù)量約束、等量數(shù)量約束等。

2）基于特定領(lǐng)域業(yè)務(wù)規(guī)則的一致性檢驗(yàn)規(guī)則

基于特定領(lǐng)域業(yè)務(wù)規(guī)則的一致性檢驗(yàn)規(guī)則用于發(fā)現(xiàn)需求模型內(nèi)存在的違反特定領(lǐng)域的業(yè)務(wù)規(guī)則。該類規(guī)則主要來自于具體作戰(zhàn)業(yè)務(wù)的條令條例和規(guī)章制度等，從描述這些規(guī)則的語法結(jié)構(gòu)上看可將其視為“IF ＜前提條件＞THEN ＜導(dǎo)致結(jié)果＞”的推理演繹規(guī)則。

另外，基于特定領(lǐng)域業(yè)務(wù)規(guī)則的一致性檢驗(yàn)規(guī)則通常采用自然語言或類自然語言描述，因此，需要將該規(guī)則轉(zhuǎn)換為可以被描述邏輯系統(tǒng)識(shí)別和理解的特定語言，即本文中采用的語義網(wǎng)規(guī)則描述語言（Semantic Web Rule Language，SWRL）［19］。領(lǐng)域業(yè)務(wù)規(guī)則的轉(zhuǎn)換算法Construct RSWRL 如下：

?

前提和結(jié)論中的概念、概念屬性、概念間關(guān)系都被轉(zhuǎn)換為Horn 子句的前題和結(jié)果，通過邏輯連接符將Horn 子句的前題和結(jié)果分別組合為SWRL 的條件和推論。需要指出的是特定領(lǐng)域業(yè)務(wù)規(guī)則的內(nèi)容和數(shù)量并無統(tǒng)一的標(biāo)準(zhǔn)規(guī)范，需求分析人員可以針對(duì)領(lǐng)域的業(yè)務(wù)特點(diǎn)定制特定領(lǐng)域業(yè)務(wù)規(guī)則，并可以在實(shí)際應(yīng)用中由領(lǐng)域?qū)＜也粩嗉右载S富和完善，隨時(shí)添加到知識(shí)庫中，因此，具備較強(qiáng)的靈活性。

4.3 需求模型的一致性推理檢驗(yàn)

針對(duì)第1 類語義層面的一致性問題，在加載本體后，需求分析人員輸入一致性查詢指令“Pellet consistency-v xxx.owl”，推理引擎會(huì)自動(dòng)執(zhí)行基于Tableaux 的一致性推理算法，判斷需求模型中存在的語義不一致性問題，并向用戶返回推理結(jié)果。

針對(duì)第2 類違反領(lǐng)域知識(shí)的一致性問題，經(jīng)推理引擎邏輯推理后，最終需要通過Abox 個(gè)體查詢方式獲得領(lǐng)域知識(shí)一致性驗(yàn)證結(jié)果。本研究針對(duì)兩類領(lǐng)域知識(shí)一致性檢驗(yàn)規(guī)則分別設(shè)計(jì)對(duì)應(yīng)的SPARQL［20］查詢語句，限制個(gè)體查詢條件，從而獲得需求分析人員關(guān)心的模型驗(yàn)證結(jié)果。

常用的SPARQL 語句結(jié)構(gòu)如下所示：

需求分析人員用每條領(lǐng)域規(guī)則對(duì)應(yīng)的SPARQL語句來查詢違反領(lǐng)域知識(shí)一致性的個(gè)體，如果該規(guī)則的查詢結(jié)果為空，表明需求模型中的數(shù)據(jù)元素滿足該規(guī)則約束，如果該規(guī)則的查詢結(jié)果不為空，則結(jié)果中的對(duì)象所代表的需求模型中的數(shù)據(jù)元素不滿足該約束。當(dāng)所有規(guī)則的查詢結(jié)果都為空時(shí)，才表明需求模型中的數(shù)據(jù)元素滿足所有的領(lǐng)域知識(shí)的約束，從而完成需求模型的一致性檢驗(yàn)。

5 案例分析

某城市一體化防空作戰(zhàn)指揮系統(tǒng)是一個(gè)典型的軍事信息系統(tǒng)，主要用于保衛(wèi)城市重要目標(biāo)免遭巡航導(dǎo)彈、空地導(dǎo)彈等突襲，形成區(qū)域防空最后一道防線的作戰(zhàn)指揮。需求分析人員在開發(fā)某城市防空一體化作戰(zhàn)系統(tǒng)時(shí)，在軍事信息系統(tǒng)概念本體引導(dǎo)下，建立領(lǐng)域概念模型，并通過實(shí)例化領(lǐng)域概念構(gòu)建某城市的防空一體化作戰(zhàn)系統(tǒng)需求模型。需求分析人員針對(duì)不同視圖可以構(gòu)建多個(gè)需求模型，從不同刻面描述該一體化防空作戰(zhàn)指揮系統(tǒng)的軍事需求。本案例為簡化問題，節(jié)選了部分領(lǐng)域概念和應(yīng)用需求概念，構(gòu)建了該系統(tǒng)的需求模型，如圖4所示。

借助于本文提出的軍事信息系統(tǒng)概念本體及需求模型的本體轉(zhuǎn)換算法將概念本體及需求模型轉(zhuǎn)換為需求本體。限于篇幅，下頁表1 僅列出部分重要公理和事實(shí)斷言。

圖4 X 防空一體化作戰(zhàn)系統(tǒng)需求模型

5.1 需求模型語義層面的一致性檢驗(yàn)問題

假設(shè)在構(gòu)建一體化防空作戰(zhàn)指揮系統(tǒng)的需求模型中，由于需求分析人員的失誤，在“快速摧毀空襲目標(biāo)DDT20”與“X 防空一體化作戰(zhàn)系統(tǒng)防空作戰(zhàn)能力x-SADC”之間錯(cuò)誤地添加了“指導(dǎo)活動(dòng)DEPA”關(guān)系，而在需求概念本體的語義約束中，“指導(dǎo)活動(dòng)DEPA”關(guān)系只存在于“預(yù)期效果Desired Effect”和“活動(dòng)Activity”之間，因此，導(dǎo)致語義層面的不一致性。

以上不一致性問題采用Pellet 1.5.0 本體推理引擎，加載本體文件“防空案例.owl”，輸入查詢命令“Pellet consistency-v 防空案例.owl”，推理引擎自動(dòng)返回如圖5 所示的推理結(jié)果。

推理界面中顯示：

圖5 X 防空一體化作戰(zhàn)系統(tǒng)需求模型一致性驗(yàn)證

結(jié)果說明“指導(dǎo)活動(dòng)”DEPA 關(guān)系本來應(yīng)該存在于實(shí)例DDT20 和Activity 的某個(gè)實(shí)例之間，而在構(gòu)建的需求模型里把DEPA 關(guān)系賦予了DDT20 和x-SADC，所以x-SADC 被錯(cuò)誤地強(qiáng)制作為Activity的實(shí)例。

5.2 領(lǐng)域知識(shí)的一致性檢驗(yàn)問題

違反領(lǐng)域知識(shí)的一致性問題又可分為違反通用領(lǐng)域知識(shí)的一致性問題和違反特定領(lǐng)域規(guī)則的一致性問題。

表1 X 防空一體化作戰(zhàn)系統(tǒng)需求本體

5.2.1 違反通用領(lǐng)域知識(shí)的一致性問題

通用領(lǐng)域規(guī)則有很多，例如：“目標(biāo)至少有一個(gè)支持其實(shí)現(xiàn)的能力”、“戰(zhàn)略目標(biāo)要分解成一個(gè)以上的使命組合”、“能力必須要有作戰(zhàn)活動(dòng)來體現(xiàn)”、“作戰(zhàn)活動(dòng)必須擁有一個(gè)執(zhí)行者”等，本案例以“作戰(zhàn)活動(dòng)必須擁有一個(gè)執(zhí)行者”為例說明通用領(lǐng)域知識(shí)的一致性檢驗(yàn)過程。此類問題通過對(duì)Abox 個(gè)體的一致性查詢來發(fā)現(xiàn)需求模型的不一致，查詢需求模型中不存在執(zhí)行者的活動(dòng)，對(duì)應(yīng)的SPARQL 查詢語句是：

向推理引擎輸入上述查詢規(guī)則，引擎返回如圖6 所示的推理結(jié)果。

結(jié)果顯示，在需求模型中存在違反此規(guī)則的個(gè)體“x-CADA”，即“X 空域防空活動(dòng)”沒有執(zhí)行者。下一步，需求分析人員需要對(duì)構(gòu)建的需求模型進(jìn)行修改，針對(duì)作戰(zhàn)想定，在“X 空域防空活動(dòng)”與某特定執(zhí)行者之間添加代表執(zhí)行關(guān)系的需求線。

圖6 X 防空一體化作戰(zhàn)系統(tǒng)需求模型通用領(lǐng)域知識(shí)一致性驗(yàn)證

5.2.2 違反特定領(lǐng)域規(guī)則的一致性問題特定領(lǐng)域規(guī)則與需求的應(yīng)用背景相關(guān)?？梢愿鶕?jù)該領(lǐng)域現(xiàn)有規(guī)章制度（如作戰(zhàn)條令條例等）或在領(lǐng)域知識(shí)框架的基礎(chǔ)上新定義一些領(lǐng)域推理檢驗(yàn)規(guī)則。

在防空作戰(zhàn)條令的導(dǎo)彈發(fā)射業(yè)務(wù)章程中規(guī)定：在導(dǎo)彈打擊任務(wù)中，任何導(dǎo)彈發(fā)射活動(dòng)的執(zhí)行必須有導(dǎo)彈發(fā)射指令作為前提條件。即如果部隊(duì)有導(dǎo)彈打擊任務(wù)并且導(dǎo)彈已經(jīng)發(fā)射，那么一定存在一條導(dǎo)彈發(fā)射指令。根據(jù)發(fā)明內(nèi)容中設(shè)計(jì)的SWRL 規(guī)則轉(zhuǎn)換算法，該條特定領(lǐng)域規(guī)則對(duì)應(yīng)的SWRL 語句為：

將上述規(guī)則導(dǎo)入公理集Tbox，需求分析人員采用Abox 個(gè)體查詢，查詢無導(dǎo)彈發(fā)射指令約束的活動(dòng)，對(duì)應(yīng)的SPARQL 查詢語句是：

引擎返回如圖7 所示的推理結(jié)果。

圖7 X 防空一體化作戰(zhàn)系統(tǒng)需求模型特定領(lǐng)域規(guī)則一致性驗(yàn)證

結(jié)果顯示，在需求模型中存在違反上述規(guī)則的個(gè)體“x-SDMLA”和“y-LDMLA”，即“x 型近程導(dǎo)彈發(fā)射活動(dòng)”和“y 型遠(yuǎn)程導(dǎo)彈發(fā)射活動(dòng)”均無導(dǎo)彈發(fā)射指令的約束。針對(duì)該不一致情況，需求分析人員需對(duì)構(gòu)建的需求模型進(jìn)行進(jìn)一步的活動(dòng)分析，在上述兩項(xiàng)導(dǎo)彈發(fā)射活動(dòng)的約束中添加相應(yīng)的發(fā)射指令。

6 結(jié)論

本文提出一種軍事信息系統(tǒng)需求模型一致性檢驗(yàn)技術(shù)，可以有效檢驗(yàn)需求分析人員所構(gòu)建的需求模型的語義是否正確，內(nèi)容是否全面如實(shí)地反映用戶要求，進(jìn)而為系統(tǒng)后續(xù)建設(shè)提供參考和決策支持。與傳統(tǒng)方法比，本方法具備以下特點(diǎn)：1）自動(dòng)化程度高。軍事信息系統(tǒng)需求模型一致性檢驗(yàn)技術(shù)基于成熟的Tableaux 算法，擁有Pellet、Protege 等多種推理引擎和工具作為支撐，保證了較高的自動(dòng)化程度；2）知識(shí)復(fù)用能力強(qiáng)。Petri 網(wǎng)、線性時(shí)序邏輯等需求分析驗(yàn)證方法均針對(duì)具體個(gè)例建模，不具備復(fù)用性。本文提出的需求概念本體及一致性檢驗(yàn)規(guī)則在構(gòu)建不同的需求模型時(shí)均可重復(fù)利用，具備較強(qiáng)的知識(shí)復(fù)用性；3）推理效率高。隨著軍事信息系統(tǒng)復(fù)雜性增加，整個(gè)系統(tǒng)產(chǎn)生的狀態(tài)量呈指數(shù)增長，線性時(shí)序邏輯等作為以窮盡搜索為基礎(chǔ)的模型檢測技術(shù)，狀態(tài)爆炸問題一直是制約其發(fā)展的瓶頸?；诿枋鲞壿嫷能娛滦畔⑾到y(tǒng)需求模型一致性檢驗(yàn)方法既可以驗(yàn)證有窮狀態(tài)系統(tǒng)，又可使用歸納的方法處理無限狀態(tài)問題，很好地規(guī)避了狀態(tài)爆炸問題。