一種面向領(lǐng)域自然語言需求的形式化需求模型生成方法研究

胡建成，胡 軍，汪文軒，康介祥，王 輝，高忠杰

1(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，南京 211106)

2(軟件新技術(shù)與產(chǎn)業(yè)化協(xié)同創(chuàng)新中心，南京 210007)

3(中國航空無線電電子研究所 軟件部，上海 200233)

1 引 言

安全關(guān)鍵軟件[1，2]是指應(yīng)用于航空、航天、交通、能源等安全關(guān)鍵系統(tǒng)領(lǐng)域中的一類軟件，此類軟件系統(tǒng)要求具有高安全性、高可靠性和高健壯性等特征[3].近年來，隨著安全關(guān)鍵系統(tǒng)的功能及復(fù)雜度的快速增長，以及軟件很小的錯誤或者漏洞可能會導(dǎo)致非常嚴(yán)重的后果[4]，例如：財(cái)產(chǎn)的重大損失、環(huán)境的嚴(yán)重破壞或者是人員的重大傷亡等.因此，如何正確有效的開發(fā)此類系統(tǒng)軟件成為了目前安全關(guān)鍵系統(tǒng)領(lǐng)域中的一個(gè)重要挑戰(zhàn).

從軟件生命周期的角度來看，在一個(gè)軟件產(chǎn)品開始的階段定義并構(gòu)造一個(gè)完整性、一致性良好的需求制品，是提高安全關(guān)鍵軟件的產(chǎn)品質(zhì)量和降低產(chǎn)品開發(fā)成本的最好方法之一.由于系統(tǒng)具備安全關(guān)鍵特征，相比較在設(shè)計(jì)或?qū)崿F(xiàn)階段引入的錯誤，在安全關(guān)鍵軟件需求中存在的錯誤更可能會對這類系統(tǒng)的安全性產(chǎn)生重要影響.以航空電子系統(tǒng)(以下簡稱航電系統(tǒng))中的軟件系統(tǒng)為例，其相應(yīng)的民用機(jī)載軟件適航標(biāo)準(zhǔn)DO-178B/C[5]中就是以多層級需求為核心來展開航電軟件研發(fā)的各類活動，并引入了最新的基于模型的系統(tǒng)/軟件工程方法學(xué)以及形式化方法[6，7]來更好的支撐達(dá)成安全性等相關(guān)目標(biāo).

本文工作就是面向航空電子系統(tǒng)領(lǐng)域，展開從自然語言描述的條目化需求到形式化需求模型生成的方法研究，包括：分析航電領(lǐng)域的需求描述特征，從該領(lǐng)域的自然語言描述的條目化需求入手，設(shè)計(jì)定義一套面向領(lǐng)域的自然語言需求模板，并綜合考慮所采用的形式化需求模型(VRM：Variable Relation Model)元素的語義，形成基于此模板的需求規(guī)范化方法；然后給出從規(guī)范化后的需求條目集到VRM模型的自動構(gòu)造方法.最后選取了現(xiàn)代民機(jī)中綜合電子顯示系統(tǒng)中的典型功能子系統(tǒng)進(jìn)行了實(shí)例需求建模及模型生成.

具體而言，本文后續(xù)內(nèi)容安排如下：第2節(jié)是本文的相關(guān)技術(shù)背景介紹，如：機(jī)載軟件適航認(rèn)證標(biāo)準(zhǔn)DO-178B/C，基于模型的分析與驗(yàn)證方法等；第3節(jié)給出了基于自然語言需求的VRM建模框架的概要說明；在第4節(jié)中對研究框架中所涉及到的關(guān)鍵概念和技術(shù)點(diǎn)進(jìn)行詳細(xì)說明，包括領(lǐng)域概念庫的語義定義、領(lǐng)域模板庫的設(shè)計(jì)以及其組成元素的數(shù)學(xué)定義、VRM模型中各類表模型的自動構(gòu)造算法等.第5節(jié)是對發(fā)動機(jī)指示和機(jī)組警告系統(tǒng)(EICAS)進(jìn)行實(shí)例分析；最后一節(jié)是相關(guān)工作比較和總結(jié).

2 相關(guān)技術(shù)背景

2.1 航空認(rèn)證標(biāo)準(zhǔn)DO-178B/C

DO-178B/C《機(jī)載系統(tǒng)和設(shè)備合格審定中的軟件考慮》標(biāo)準(zhǔn)是美國航空無線電委員會(RTCA)發(fā)布的民機(jī)軟件系統(tǒng)開發(fā)的工業(yè)開發(fā)指南.其中以過程和目標(biāo)為核心概念來給出航電軟件研發(fā)中所關(guān)注的重點(diǎn)，尤其強(qiáng)調(diào)各層級需求(系統(tǒng)需求、軟件高級需求、軟件低級需求等)是航電軟件研發(fā)中的重中之重.在最新的DO-178C標(biāo)準(zhǔn)中還專門增加了基于模型開發(fā)方法的支持(DO-331附件標(biāo)準(zhǔn))[8]、面向?qū)ο?DO-332附件標(biāo)準(zhǔn))[9]和形式化方法(DO-333附件標(biāo)準(zhǔn))[10]，進(jìn)一步引入了以需求為核心的雙向追溯機(jī)制.

在DO-333中所引入的形式化方法是用于開發(fā)計(jì)算機(jī)硬件和軟件系統(tǒng)的一類數(shù)學(xué)技術(shù)，通常分為模型檢測、定理證明以及抽象解釋等3大類方法.數(shù)學(xué)方法的嚴(yán)格性可以支持計(jì)算機(jī)系統(tǒng)研發(fā)項(xiàng)目生命周期中涉及到的不同層次上的模型分析.尤其是在需求與架構(gòu)設(shè)計(jì)階段，形式化方法可以用于準(zhǔn)確的獲取、解釋和描述需求及其相應(yīng)的約束.在本文工作中所應(yīng)用的VRM模型是基于四變量模型[11]的核心語義，并面向航電軟件進(jìn)行領(lǐng)域化裁剪之后的形式化模型，其詳細(xì)說明參見3.2小節(jié).

2.2 基于模型的分析與驗(yàn)證

基于模型的系統(tǒng)/軟件工程(Model Based System Engineering，MBSE)是通過建立多層級的建模與轉(zhuǎn)換[12]，從系統(tǒng)/軟件的概念設(shè)計(jì)階段開始支持系統(tǒng)/軟件需求、設(shè)計(jì)、分析、驗(yàn)證和確認(rèn)等活動，并持續(xù)貫穿整個(gè)開發(fā)過程和后續(xù)的生命周期階段.MBSE方法是從用戶需求開始將系統(tǒng)逐層分解為各子系統(tǒng)、部件和模塊等，并建立各類系統(tǒng)/軟件的模型，最后進(jìn)行各子系統(tǒng)和模塊的實(shí)現(xiàn)，進(jìn)行集成和驗(yàn)證，形成系統(tǒng)并進(jìn)行確認(rèn)，得到符合用戶需求的系統(tǒng)產(chǎn)品.

一個(gè)完整項(xiàng)目的開發(fā)與實(shí)現(xiàn)，往往需要很多團(tuán)隊(duì)的合作共同去實(shí)現(xiàn).通過MBSE方法框架，可以更好的進(jìn)行技術(shù)活動的計(jì)劃、組織、協(xié)調(diào)和控制，同時(shí)統(tǒng)籌各種資源的分配，有助于提高項(xiàng)目軟件的生產(chǎn)效率，降低開發(fā)成本.本文工作的關(guān)注重點(diǎn)就是在需求層級，圍繞如何從自然語言描述的需求建立有效的形式化需求模型進(jìn)行展開.

3 面向領(lǐng)域自然語言需求的VRM建模

在本小節(jié)中首先給出了面向領(lǐng)域自然語言需求的形式化需求模型(VRM)的建?？蚣?包括在此框架中的自然語言需求模板化處理和從模板化需求到VRM形式化模型的自動構(gòu)造兩部分內(nèi)容的總體說明.然后給出了本建?？蚣苤行问交枨竽Ｐ?VRM)的概要說明.

3.1 面向領(lǐng)域自然語言建模的框架

本文工作內(nèi)容是屬于一個(gè)總體項(xiàng)目ART(Avionics Requirement Tools)的研究內(nèi)容的一部分(如圖1所示).整個(gè)項(xiàng)目的目標(biāo)是面向DO-178C標(biāo)準(zhǔn)，設(shè)計(jì)并實(shí)現(xiàn)一個(gè)滿足標(biāo)準(zhǔn)中需求分析與驗(yàn)證要求的軟件工具平臺(ART).首先，在需求建模階段，需要考慮現(xiàn)代民機(jī)航電軟件需求中的領(lǐng)域特征，面向自然語言描述的航電領(lǐng)域需求條目，以“四變量理論模型”形式化方法為核心，給出一種構(gòu)建包含條件、事件、模式、環(huán)境交互等要素的工程實(shí)用的形式化需求模型的建模方法(VRM).然后基于VRM的形式化語義，對需求模型展開一致性、完整性等性質(zhì)的分析與驗(yàn)證.最后，經(jīng)過形式化分析的VRM需求模型就可以用來自動生成測試用例集.

圖1 航電軟件需求工具ART

具體而言，本文工作內(nèi)容重點(diǎn)就是針對高安全性的航電軟件領(lǐng)域，提出一種面向領(lǐng)域自然語言需求的需求規(guī)范化方法，然后對規(guī)范化后的需求模型進(jìn)行解析，提取其中包括條件、事件、模式等在內(nèi)的核心信息，綜合領(lǐng)域概念庫的內(nèi)容，設(shè)計(jì)了VRM模型自動構(gòu)造算法來生成形式化需求模型.總體框架如圖2所示，包括：面向領(lǐng)域的自然語言需求模板化處理和模板化的需求到VRM形式化模型的自動構(gòu)造兩大部分.以下分別說明.

圖2 面向領(lǐng)域自然語言的VRM模型生成方法研究框架

首先，面向領(lǐng)域自然語言需求，設(shè)計(jì)定義一套領(lǐng)域自然語言需求模板，對自然語言需求進(jìn)行規(guī)約，得到規(guī)范化需求模型.領(lǐng)域自然語言需求模板是根據(jù)領(lǐng)域相關(guān)知識和實(shí)際應(yīng)用需求進(jìn)行定義.它是將需求文檔中所包含的各種數(shù)據(jù)、專有名詞以及固定句式利用模板和形式化語義進(jìn)行定義，使得工程人員采用統(tǒng)一且規(guī)范的方法描述需求，從而達(dá)到減少需求定義過程中所造成的人為失誤.領(lǐng)域自然語言需求模板內(nèi)容包括：領(lǐng)域概念庫和領(lǐng)域模板庫.

1)領(lǐng)域概念庫中主要包括：專有名詞，常量，輸入變量、輸出變量，中間變量，模式集.其中，專有名詞指的是領(lǐng)域特有的系統(tǒng)名、組件名等；常量描述的是需求中預(yù)先定義的一些常數(shù).輸入變量指的是系統(tǒng)狀態(tài)轉(zhuǎn)換過程中，動態(tài)輸入的數(shù)據(jù)；輸出變量指的是系統(tǒng)狀態(tài)轉(zhuǎn)換過程中，值發(fā)生改變的一類數(shù)據(jù)；中間變量指的是有些輸入數(shù)據(jù)需要經(jīng)過一系列的運(yùn)算才能最終產(chǎn)生輸出數(shù)據(jù)，為了更好的描述這一過程，添加了中間變量對其進(jìn)行補(bǔ)充描述.模式集是N個(gè)非空不相交的模式的并集，每個(gè)模式都是系統(tǒng)狀態(tài)的等價(jià)類.

2)領(lǐng)域模板庫結(jié)合了領(lǐng)域自然語言需求的句式特征和VRM模型元素的語義特征，設(shè)計(jì)定義了4種類型模板，分別為：通用條件型模板、通用事件型模板、顯示條件型模板和顯示事件型模板.

3)利用定義好的領(lǐng)域概念庫和領(lǐng)域模板庫，對特定領(lǐng)域自然語言需求進(jìn)行規(guī)約，得到可轉(zhuǎn)換為形式化模型的規(guī)范化需求.這里的規(guī)約，本質(zhì)上來講是對一般形式的自然語言描述的需求，按照預(yù)定義的需求模板的語義和語法形式，由需求建模人員來進(jìn)行語義等價(jià)的需求條目的模板化、規(guī)范化的重構(gòu)過程.其最終目的是規(guī)約后的需求條目，可進(jìn)行后續(xù)內(nèi)容：使用算法來自動構(gòu)造VRM需求模型(詳細(xì)的需求規(guī)約過程見5.2節(jié)實(shí)例分析).這個(gè)規(guī)約過程以及過程中所用到的模板是建立在領(lǐng)域知識和VRM模型方法論的基礎(chǔ)上，目前主要適用于航電軟件這類安全關(guān)鍵系統(tǒng)需求建模與分析.

其次，基于規(guī)范化需求模型及VRM模型的基本特征，定義了規(guī)范化需求模型和VRM模型的數(shù)據(jù)結(jié)構(gòu).利用VRM模型的自動構(gòu)造算法，將規(guī)范化需求模型自動構(gòu)造為VRM模型.

1)利用正則表達(dá)式定義領(lǐng)域模板庫，從而將需求規(guī)約過程中所得到的規(guī)范化需求模型進(jìn)行解析，由此得到需求模型元素，例如：輸入變量領(lǐng)域概念、輸出變量領(lǐng)域概念等.

2)將解析得到的需求模型元素，利用預(yù)定義的需求模型元素-VRM模型元素映射表以及領(lǐng)域自然語言需求模板-VRM表格函數(shù)映射表進(jìn)行映射，由此得到VRM模型元素及構(gòu)建VRM模型表格函數(shù)的相關(guān)信息.

3)將得到的VRM模型元素及構(gòu)建VRM模型表格函數(shù)的相關(guān)信息進(jìn)行模型自動化構(gòu)建，形成VRM模型.

3.2 VRM建模

當(dāng)前各種形式化方法和理論很多，但是來源于實(shí)際工程，并能真正應(yīng)用于實(shí)際工程領(lǐng)域中的需求描述方法很少.并且大多數(shù)形式化方法大都采用各種很陌生的符號和邏輯公式來表達(dá)模型，這使得絕大多數(shù)的形式化方法很難被現(xiàn)有的系統(tǒng)工程人員所理解接受.事實(shí)上，工程人員最了解的是工程領(lǐng)域知識，而且在航電系統(tǒng)工程領(lǐng)域中最常見使用的就是各種表格形式(如：各種航電系統(tǒng)操作手冊、飛行手冊等等)，工程人員最熟悉的也是表格.因此，本文工作中采用的VRM模型就是同時(shí)具備表格化和形式化語義的需求模型.

類似于在關(guān)系數(shù)據(jù)庫中的數(shù)據(jù)存儲處理方式，VRM模型的直觀形式是采用二維表格來建立需求模型.關(guān)系數(shù)據(jù)庫中的二維關(guān)系數(shù)據(jù)事實(shí)上是由關(guān)系演算邏輯系統(tǒng)來嚴(yán)格定義好的數(shù)學(xué)模型(即：形式化模型).VRM是基于四變量模型，并根據(jù)航電軟件領(lǐng)域特征進(jìn)行了剪裁所得到的，其中部分內(nèi)容的形式化定義如下：

VRM需求規(guī)約的六元組：{SV，C，E，F(xiàn)，TS，VR}.其中SV是所有狀態(tài)變量的集合，為一個(gè)四元組，定義為：SV={MV，CV，M，IV}，包含輸入變量MV、輸出變量CV、模式集M，中間變量IV.下面具體介紹六元組每個(gè)數(shù)據(jù)的功能.

MV：非空的不相交的輸入變量的集合，MV={mv1，mv2，…，mvl}，mv1，mv2，…，mvl稱為輸入變量；

CV：非空的不相交的輸出變量的集合，CV={cv1，cv2，…，cvl}，cv1，cv2，…，cvl稱為輸出變量；

M：非空的不相交的模式集的集合，M={mc1，mc2，…，mcm}，mc1，mc2，…，mcm稱為模式，其中mci為某個(gè)模式集，它包含了該模式集下的所有模式，Mci={mci1，mci2，…，mcim}；

IV：非空的不相交的中間變量的集合，IV={iv1，iv2，…，ivk}，iv1，iv2，…，ivk稱為中間變量；

TS：類型的并集，其中所有的類型都是值的非空集合.

VR：特殊的函數(shù)，用來將狀態(tài)變量的名稱映射到具體的值，表示狀態(tài)變量的所有取值范圍.對于VR中的所有r∈VR(r)，r是SV中的某個(gè)變量，TS 是r的值域類型.VR(r)是r可能取值的集合.

C：條件，表示單個(gè)狀態(tài)變量上的謂詞，如Altitude>500表示當(dāng)前的高度大于500.條件是邏輯表達(dá)式，具有多種表達(dá)形式，可以為布爾變量true、false或布爾表達(dá)式ci⊙cj等.⊙∈{AND，OR，NOT}表示邏輯操作符；ci=r° v.其中° ∈{=，<，>，≠，≥，≤}表示關(guān)系操作符.

E：事件，表示兩個(gè)狀態(tài)變量上的謂詞，事件的通用表達(dá)式為：

EVENT(S)GUARDD.

EVENT∈{@T，@F，@C}表示事件操作符；GUARD∈{WHEN，WHERE，WHILE}表示守衛(wèi)操作符；

F：表格函數(shù)，所有的表格都是一個(gè)數(shù)學(xué)函數(shù)，都可以使用Fi表示.

在VRM模型中，表格函數(shù)包括3大類：條件表，事件表和模式轉(zhuǎn)換表.這3類表都有相應(yīng)的形式化語義定義.限于篇幅，以下僅以示例1和示例2給出簡要概述.示例1是一個(gè)條件表的例子，語義為：基于狀態(tài)依賴關(guān)系Dn={Pressure，Overriden}定義了輸出變量SafetyInjection的取值情況(即某個(gè)功能需求F1).其對應(yīng)的二維表用于直觀表示數(shù)據(jù)邏輯公式語義的形式化模型(見表1).

表1 條件表示例

示例1.

SafetyInjection=F1(Pressure，Overridden)=

{Off if Pressure=high∨Pressure=Permitted∨(

Pressure=TooLow∧Overridden=true)

On if Pressure=TooLow∧Overridden=false

}

示例2則給出一個(gè)事件表的例子，是基于新舊狀態(tài)依賴關(guān)系集合：{Block，Reset，Pressure，Overriden}和{Block，Reset，Pressure}，函數(shù)定義了輸出變量Overridden的值(即某個(gè)功能需求F2).其對應(yīng)的二維表用于直觀表示數(shù)據(jù)邏輯公式語義的形式化模型(見表2).

表2 事件表示例

示例2.

Overridden=F2(Pressure，Block，Reset，Block′

Overridden，Pressure′，Reset′)=

{true if(Block′=On∧Block=Off∧Pressure

=TooLow∧Reset=Off)∨(Block′=On

∧Block=Off∧Pressure=Permitted

∧Reset=Off)

false if(Reset′=On∧Reset=Off∧Pressure

=TooLow)∨(Reset′=On∧Reset=Off

∧Pressure=Permitted)∨(Pressure′=

High∧Pressure≠High)∨((Presurre′=

Permitted∨Pressure′=TooLow)∧(

Pressure=Permmited∨Pressure=

TooLow))

Overridden otherwise(no change)

}

4 建模框架中的核心問題

在本小節(jié)中對第3章節(jié)研究框架中所涉及到的關(guān)鍵概念，進(jìn)行詳細(xì)的設(shè)計(jì)定義.首先，介紹了使用N元組的形式定義領(lǐng)域概念庫中的具體內(nèi)容；其次，表述了領(lǐng)域模板庫的具體內(nèi)容，以及其組成元素的數(shù)學(xué)定義；最后描述了VRM模型自動構(gòu)造的算法及其說明.

4.1 領(lǐng)域概念庫

領(lǐng)域概念庫是建立在具體的領(lǐng)域及實(shí)際的需求中，將需求中所涉及的對象名詞，領(lǐng)域概念以及各種數(shù)據(jù)集中起來，采用規(guī)范且符合形式化語義的形式對它們的屬性進(jìn)行描述.領(lǐng)域概念庫包含如下內(nèi)容：專有名詞、常量、變量和模式集，其中變量又分為輸入變量、輸出變量和中間變量，模式繼承模式集.

專有名詞和對象名稱之間是一一對應(yīng)的關(guān)系，例如：EICAS系統(tǒng)中顯示功能(對象名稱)與專有名詞“顯示”一一對應(yīng).模式集是VRM模型中的一個(gè)核心概念，是用來刻畫復(fù)雜的安全關(guān)鍵系統(tǒng)在運(yùn)行時(shí)候可能處于多種不同的運(yùn)行模式下(例如：空調(diào)有制冷模式集和制熱模式集，制冷模式集又包括強(qiáng)風(fēng)和弱風(fēng)等模式).模式集的構(gòu)造事實(shí)上是依據(jù)VRM模型模式集的建模思想，由需求建模人員對特定領(lǐng)域中系統(tǒng)的運(yùn)行方式展開基于模式集的分析而建立起來的，VRM模型中模式集的建模概念是提供了一種指導(dǎo)性的模式集構(gòu)造的框架.不同的需求對象的領(lǐng)域概念庫的建立都是來自于工程經(jīng)驗(yàn)的積累，并沒有規(guī)則.

本文采取面向?qū)ο笾蓄惗x的思想對領(lǐng)域概念庫中的內(nèi)容進(jìn)行定義，如圖3所示，并采用N元組的形式進(jìn)行表示(見表3).

表3 領(lǐng)域概念庫語義定義

圖3 領(lǐng)域概念庫層級關(guān)系

領(lǐng)域概念庫中所包含的常量及變量定義式中的數(shù)據(jù)類型(Datatype)，包括系統(tǒng)預(yù)定義及用戶自定義兩部分內(nèi)容.系統(tǒng)預(yù)定義部分包括Boolean，Char，F(xiàn)loat，Double，Integer，String和Unsigned.用戶自定義數(shù)據(jù)類型是在系統(tǒng)預(yù)定義數(shù)據(jù)類型的基礎(chǔ)上，對值域和精度進(jìn)行重定義，得到新的更符合實(shí)際工程使用的數(shù)據(jù)類型.新的數(shù)據(jù)類型定義內(nèi)容包括：數(shù)據(jù)類型的名稱，類型，值域和精度.可重定義的數(shù)據(jù)類型包括：Char，Integer，F(xiàn)loat，Double，Unsigned和Enumerated.

例如EICAS系統(tǒng)中原始需求，“當(dāng)ipFADECEngineManualThrottleCmd等于TRUE時(shí)，發(fā)動機(jī)顯示器推力參考的圖形符號的顏色應(yīng)為Green 100.”.其中包含：一個(gè)輸入變量：ipFADECEngineManualThrottleCmd，一個(gè)輸出變量：opFADECEngineThrustReferenceGraphicColor(來自：發(fā)動機(jī)顯示器推力參考的圖形符號顏色)以及一個(gè)自定義數(shù)據(jù)類型color(來自：Green100).該條需求的領(lǐng)域概念庫的詳細(xì)定義如表4所示.

表4 需求示例領(lǐng)域概念庫

4.2 領(lǐng)域模板庫

領(lǐng)域模板庫是采用固定的句式對需求進(jìn)行規(guī)范化描述.本文綜合考慮了航空工業(yè)領(lǐng)域的需求描述標(biāo)準(zhǔn)，對EICAS系統(tǒng)的需求特征進(jìn)行分析，將其分為4個(gè)基本類型：通用型需求，顯示型需求，功能型需求和其它需求.

4.2.1 領(lǐng)域模板

根據(jù)對已有的EICAS需求實(shí)例進(jìn)行統(tǒng)計(jì)，發(fā)現(xiàn)實(shí)際需求中多為通用型需求和顯示型需求.根據(jù)VRM模型的特征，例如：條件表和事件表等.因此，設(shè)計(jì)了4個(gè)基本的領(lǐng)域模板.

1)通用條件：當(dāng)滿足以下條件，<飛機(jī)/系統(tǒng)/設(shè)備>應(yīng)能夠<功能><對象>：<條件>.

2)通用事件：當(dāng)發(fā)生以下事件，<飛機(jī)/系統(tǒng)/設(shè)備>應(yīng)能夠<功能><對象>：<事件>.

3)顯示條件：當(dāng)滿足以下條件，<對象>應(yīng)能夠<功能><格式/要求/標(biāo)準(zhǔn)>：<條件>.

4)顯示事件：當(dāng)發(fā)生以下事件，<對象>應(yīng)能夠<功能><格式/要求/標(biāo)準(zhǔn)>：<事件>.

需求模板中所使用的<飛機(jī)/系統(tǒng)/設(shè)備>、<對象>、<格式/要求/標(biāo)準(zhǔn)>和<功能>皆為領(lǐng)域概念庫中的領(lǐng)域概念，例如：<飛機(jī)/系統(tǒng)/設(shè)備>就是輸出變量和中間變量領(lǐng)域概念.他們已在4.1節(jié)進(jìn)行過嚴(yán)格的定義.<條件>及<事件>的形式化語義將在4.2.2和4.2.3進(jìn)行定義.

下面以顯示條件模板進(jìn)行舉例說明.例如4.1節(jié)中的示例，“opFADECEngineThrustReferenceGraphicColor”對應(yīng)于<對象>，“Green 100”對應(yīng)于<格式/要求/標(biāo)準(zhǔn)>，“顯示”對應(yīng)于<功能>，“ipFADECEngineManualThrottleCmd等于true時(shí)”對應(yīng)于<條件>.

本文定義的領(lǐng)域模板是在對已有的EICAS實(shí)際需求，綜合航空工業(yè)領(lǐng)域標(biāo)準(zhǔn)、需求特征及VRM模型特征所定義的.后續(xù)工作中根據(jù)更多的領(lǐng)域特征，綜合提煉出更加全面的模板，進(jìn)而豐富領(lǐng)域模板的內(nèi)容.

4.2.2 條件模板

條件指的是數(shù)據(jù)項(xiàng)的取值.條件可能是復(fù)合的，即它們是由簡單條件組成，并通過邏輯運(yùn)算符AND，OR，NOT進(jìn)行連接.

簡單條件模板使用三元組定義如下：

ci=(O，R，V)

1)O(Object)：對象，通常為領(lǐng)域概念庫中的輸入變量.

2)R(Relation)：關(guān)系操作，如：=，<，>，>=，<=等.

3)V(Value)：值，是指輸入變量取值范圍內(nèi)的一個(gè)具體取值.

因此，條件模板采用如下的BNF范式進(jìn)行定義.c表示簡單條件，C_term表示組成條件的項(xiàng)，C表示條件.

c：：=object ′>′ value | object ′<′ value | object ′=′ value | object ′<=′ value | object ′>=′ value

C_term：：=[NOT]c | C_term AND C_term | C_term OR C_term

C：：=C_term | C AND C_term | C OR C_term

例如4.1節(jié)中給出的EICAS需求示例的條件可表示為：ipFADECEngineManualThrottleCmd = true.

4.2.3 事件模板

在實(shí)際需求中，存在這樣的一類需求，它無法使用簡單的條件對其進(jìn)行表達(dá)，需要引入一種新的描述機(jī)制：事件.例如：當(dāng)高度低于500時(shí)，只要求報(bào)警器報(bào)警3秒鐘，隨后不再報(bào)警.如果使用條件形式表述，則會出現(xiàn)錯誤，且報(bào)警器會一直處于報(bào)警狀態(tài)，與實(shí)際需求所描述的語義不同.所以，此處應(yīng)該使用事件的形式進(jìn)行表達(dá).

根據(jù)3.2節(jié)中<事件>表達(dá)式的定義，單個(gè)事件有3種：@T，@F和@C.事件操作符和守衛(wèi)操作符兩兩組合，有9種，共計(jì)12種.

1)@T：表示上一狀態(tài)_S的值為FALSE，當(dāng)前狀態(tài)S為TRUE的事件.即：NOT _S AND S.

2)@F：表示上一狀態(tài)_S的值為TRUE，當(dāng)前狀態(tài)S為FALSE的事件.即：_S AND NOT S.

3)@C：表示當(dāng)S上一狀態(tài)的值不等于當(dāng)前狀態(tài)的時(shí)的事件.即：S ！= _S.

4)WHEN：表示上一狀態(tài)D為真.

5)WHILE：表示當(dāng)前狀態(tài)D為真.

6)WHERE：表示上一狀態(tài)和當(dāng)前狀態(tài)皆為真.

例如：@T(S)WHEN(D)，表示S上一狀態(tài)為假，當(dāng)前狀態(tài)為真，且D上一狀態(tài)為真.

因此，得到事件模板如表5所示.

表5 事件模板

4.3 模型構(gòu)造

從規(guī)范化需求模型到VRM模型自動構(gòu)造的過程主要包括兩部分：

1)領(lǐng)域概念庫的轉(zhuǎn)換：領(lǐng)域概念庫轉(zhuǎn)換到VRM模型中的常量字典、變量字典和用戶自定義類型.例如：4.1中示例發(fā)動機(jī)顯示器推力參考的圖形符號顏色，在領(lǐng)域概念庫中為輸出變量，需轉(zhuǎn)換到VRM模型中變量字典的輸出變量.領(lǐng)域概念庫與VRM模型中的數(shù)據(jù)字典為一一對應(yīng)的關(guān)系.

2)規(guī)范化需求的轉(zhuǎn)換：領(lǐng)域自然語言需求經(jīng)過需求模板的規(guī)約操作后，所得到的規(guī)范化需求語義為，“在某個(gè)條件或者事件下，某個(gè)變量(變量為輸出變量或者中間變量)取得其值域范圍內(nèi)的一個(gè)具體值”.而輸出變量、中間變量的值域應(yīng)至少包含一個(gè)數(shù)據(jù)，所以規(guī)范化需求與VRM模型的表格函數(shù)為多對一的轉(zhuǎn)換關(guān)系.

4.3.1 規(guī)范化需求模型

基于上述兩個(gè)章節(jié)定義的內(nèi)容，給出規(guī)范化需求模型數(shù)據(jù)結(jié)構(gòu)如圖4所示.

規(guī)范化需求模型主要分為兩個(gè)部分：領(lǐng)域概念庫和規(guī)范化需求.領(lǐng)域概念庫包含常量概念庫、自定義數(shù)據(jù)類型概念庫、輸入變量概念庫、中間變量概念庫、輸出變量概念庫、模式集概念庫、模式概念庫和模式轉(zhuǎn)換概念庫.規(guī)范化需求包括通用條件型規(guī)范化需求、通用事件型規(guī)范化需求、顯示條件規(guī)范化需求和顯示事件規(guī)范化需求.

4.3.2 VRM模型

VRM模型包括常量字典、自定義數(shù)據(jù)類型、變量字典和行為表.為更好的表達(dá)模型信息以及后續(xù)工具的具體實(shí)現(xiàn)，對其內(nèi)容進(jìn)行了整合，轉(zhuǎn)換為常量字典、自定義數(shù)據(jù)類型、輸入變量字典、輸出變量(中間變量)條件表、輸出變量(中間變量)事件表及模式轉(zhuǎn)換表.綜上，給出VRM模型數(shù)據(jù)結(jié)構(gòu)如圖5所示.

圖5 VRM模型數(shù)據(jù)結(jié)構(gòu)

4.3.3 VRM模型構(gòu)造

VRM模型構(gòu)造分為3種類型：

1)常量字典、自定義數(shù)據(jù)類型和輸入變量字典的構(gòu)造.以常量字典為例，構(gòu)造算法見算法1.

算法1.生成常量字典

輸入：ConceptConst

輸出：DictionaryConst

1.foreach ConceptConst cc in arrayConceptConstdo

2. DictionaryConstDataValue = cc.getValue()；

3. dc.setDictionaryConst()；

4. arrayDC.add(dc)；

5.endfor；

常量字典構(gòu)造算法的輸入為常量領(lǐng)域概念，輸出為常量字典.單個(gè)的常量使用4.3.2章節(jié)中定義的常量字典類的實(shí)例化對象進(jìn)行存儲，常量字典則為常量對象所組成的常量對象數(shù)組.通過對常量領(lǐng)域概念對象數(shù)組進(jìn)行遍歷，將其中所包含的常量字典語義信息進(jìn)行轉(zhuǎn)換.因?yàn)橹贿M(jìn)行了一次循環(huán)，故算法復(fù)雜度為O(n).

2)行為表：輸出變量(中間變量)條件表和輸出變量(中間變量)事件表的構(gòu)造.構(gòu)造算法見算法2.

算法2.生成行為表

輸入：ConceptTermVariable.ConceptOutputVariable.StandardRequirement.

輸出：BehaviorTable

1.foreach ConceptVariable cv in arrayConceptVariabledo

2. DictionaryVariableDataValue = cv.getValue()；

3.foreach StandardRequirement sr in arraySRdo

4.ifsr.getVariableName().equals(cv.getName())then

5.ifsr.getReqType.euqals("Condition")do

6. ConditionDataValue = sr.getValue()；

7. c.setCondition()；

8. arrayC.add(c)；

9.endif

10.ifsr.getReqType.equals("Event")do

11. EventDataValue = sr.getValue()；

12. e.setEvent()；

13. arrayE.add(e)；

14.endif

15.endif

16.endfor

17. bt.setBehaviorTable()；

18. arrayBT.add(bt)；

18. arrayC = new ArrayList ()；

19. arrayE = new ArrayList ()；

20.endfor

行為表構(gòu)造算法輸入為中間變量領(lǐng)域概念，輸出變量領(lǐng)域概念和規(guī)范化需求，輸出為VRM行為表，包括：中間變量條件表、中間變量事件表、輸出變量條件表和輸出變量事件表.中間變量領(lǐng)域概念和輸出變量領(lǐng)域概念合并存儲為變量領(lǐng)域概念.行為表中主要包含兩方面內(nèi)容：變量領(lǐng)域概念內(nèi)容和規(guī)范化需求中包含的行為信息(條件和事件).因此，定義了條件對象數(shù)組、事件對象數(shù)組以及行為表對象數(shù)組.

算法的主要處理過程是先對變量領(lǐng)域概念進(jìn)行遍歷，獲取行為表中變量的相關(guān)信息.因?yàn)橐粋€(gè)變量中可能包含條件表或者事件表信息，所以，第2個(gè)循環(huán)中對規(guī)范化需求進(jìn)行遍歷，查找與該變量相關(guān)的規(guī)范化需求，判斷此需求是條件型需求或是事件型需求，將其信息存儲到條件或事件對象數(shù)組中.最后，將獲取到的信息賦值到行為表對象中構(gòu)成行為表對象數(shù)組.因?yàn)檫M(jìn)行了兩層循環(huán)，所以算法復(fù)雜度為O(n2).

3)模式轉(zhuǎn)換表的構(gòu)造.構(gòu)造算法見算法3.

算法3.生成模式轉(zhuǎn)換表

輸入：ConceptModeClass、ConceptMode、ConceptModeTran-sition.

輸出：ModeMachine

1.foreach ConceptModeClass mc in arrayMCdo

2. ModeClassDataValue = mc.getValue()；

3.foreach ConceptMode cm in arrayCMdo

4.ifcm.getModeClassName.equals(mc.getName())then

5. ModeDataValue = cm.getValue()；

6. m.setMode()；

7. arrayM.add(m)；

9.endif

10.endfor

11.foreach ConceptModeTransition cmt in arrayCMTdo

12.ifcmt.getModeClassName.equals(mc.getName())then

13. BehaviorModeTransitionDataValue=cmt.getValue()；

14. bmt.setBehaviorModeTransition()；

15. arrayBMT.add(bmt)；

16.endif

17.endfor

18. mm.setModeMachine()；

19. arrayMM.add(mm)；

20.arrayM = new arrayList ()；

21.arrayBMT = new arrayList

22.endfor

模式轉(zhuǎn)換表構(gòu)造算法輸入為模式集領(lǐng)域概念，模式領(lǐng)域概念和模式轉(zhuǎn)換領(lǐng)域概念，輸出為模式轉(zhuǎn)換表.模式轉(zhuǎn)換表中包含了模式集信息、模式集所包含的模式和模式在相關(guān)事件下的轉(zhuǎn)換信息.因此，定義了模式對象數(shù)組用于保存模式集下的模式，模式轉(zhuǎn)換對象數(shù)組用于保存模式集下的模式之間的轉(zhuǎn)換信息.

算法的主要處理過程是先對模式集領(lǐng)域概念進(jìn)行遍歷，獲取模式轉(zhuǎn)換表中模式集的相關(guān)信息.因?yàn)橐粋€(gè)模式集中包含多個(gè)模式，所以對模式領(lǐng)域概念進(jìn)行遍歷，獲取其中屬于當(dāng)前模式集的相關(guān)模式，構(gòu)成模式對象數(shù)組.同時(shí)，當(dāng)前模式集下的模式之間的轉(zhuǎn)換可能存在多個(gè)，所以對模式轉(zhuǎn)換領(lǐng)域概念進(jìn)行遍歷，獲取屬于當(dāng)前模式集的模式轉(zhuǎn)換數(shù)據(jù)構(gòu)成模式轉(zhuǎn)換對象數(shù)組.最終形成模式轉(zhuǎn)換表對象數(shù)組.因?yàn)檫M(jìn)行了兩層循環(huán)，所以算法復(fù)雜度為O(n2).

5 EICAS實(shí)例分析

5.1 EICAS系統(tǒng)概述

發(fā)動機(jī)指示和機(jī)組警告系統(tǒng)(EICAS，Engine-Indicating and Crew Alerting System)，用來指示飛機(jī)各系統(tǒng)工作狀態(tài)，提供文字、圖形和音頻信息，出現(xiàn)故障時(shí)提示故障和發(fā)出警告.EICAS分兩個(gè)區(qū)域：發(fā)動機(jī)指示和機(jī)組警告信息.發(fā)動機(jī)指示區(qū)域包含發(fā)動機(jī)參數(shù)及襟翼位置、燃油量、起落架位置信息等；機(jī)組警告信息顯示EICAS的右上角，用來提示警示信息和警告信息等.

5.2 EICAS VRM模型生成

考慮到文本篇幅，此處選取實(shí)際需求中的一部分需求進(jìn)行模型的構(gòu)建及模型的轉(zhuǎn)換工作實(shí)例分析.

自然語言原始需求條目.

1)當(dāng)(參數(shù)ipFlightDeckUnitsConfigurationIsMetric有效并且等于TRUE)時(shí)，飛機(jī)綜合電子顯示系統(tǒng)應(yīng)將參數(shù)ipFlightDeckUnitsConfigurationIsMetric設(shè)置為METRIC，否則設(shè)置為IMPERIAL.

2)當(dāng)ipFADECEngineManualThrottleCmd等于TRUE時(shí)，發(fā)動機(jī)顯示器推力參考的圖形符號的顏色應(yīng)為Green 100.

3)如果值ipFADECEngineThrust[L | R]遠(yuǎn)離值ipFADECEngineThrustCommand[L | R]，則發(fā)動機(jī)顯示器應(yīng)顯示顏色黃色50的命令扇區(qū).

對以上3條原始需求進(jìn)行領(lǐng)域概念庫的構(gòu)建，得到表6-表9的內(nèi)容.

表6 輸入變量領(lǐng)域概念

表7 輸出變量領(lǐng)域概念

表8 中間變量領(lǐng)域概念

表9 自定義數(shù)據(jù)類型

根據(jù)4.2章節(jié)定義的領(lǐng)域模板庫以及上述定義的領(lǐng)域概念庫，對原始需求進(jìn)行需求規(guī)約，得到如下規(guī)范化需求條目：

1)當(dāng)滿足以下條件，opFDUConfigurationFormat應(yīng)能夠設(shè)置為METRIC：ipFDUConfigurationIsMetric = TRUE AND ipFDUConfigurationIsMetricStatus = Valid.

2)當(dāng)滿足以下條件，opFDUConfigurationFormat應(yīng)能夠設(shè)置為IMPERIAL：ipFDUConfigurationIsMetric = FALSE AND ipFDUConfigurationIsMetricStatus = Valid.

3)當(dāng)滿足以下條件，opFDUConfigurationFormat應(yīng)能夠設(shè)置為IMPERIAL：ipFDUConfigurationIsMetric = FALSE AND ipFDUConfigurationIsMetricStatus = Invalid.

4)當(dāng)滿足以下條件，opFDUConfigurationFormat應(yīng)能夠設(shè)置為IMPERIAL：ipFDUConfigurationIsMetric = TRUE AND ipFDUConfigurationIsMetricStatus = Invalid.

5)當(dāng)滿足以下條件，opFADECEngineThrustReferenceGraphicColor應(yīng)能夠顯示為Green 100：ipFADECEngineManualThrottleCmd = TRUE.

6)當(dāng)滿足以下事件，opN1CommandSectorColor應(yīng)能夠顯示為黃色 50：@C(tAbsoluteValueCommandAndThrust)when(tAbsoluteValueCommandAndThrust = increasing).

利用VRM模型自動構(gòu)造算法，對上述得到的規(guī)范化需求及領(lǐng)域概念庫內(nèi)容進(jìn)行轉(zhuǎn)換，得到VRM模型.

上述過程在工具中最終得到的模型如圖6所示.

圖6 VRM模型

6 相關(guān)工作與小結(jié)

目前在航電應(yīng)用領(lǐng)域，從系統(tǒng)及軟件需求建模的角度來看，相關(guān)工作大致分為如下幾類：1)從實(shí)際的安全關(guān)鍵系統(tǒng)的工程開發(fā)經(jīng)驗(yàn)中形成的理論與技術(shù)，如：四變量模型[13]、SCR方法[14]、RSML方法[15]、CoRE方法[16]、SpecTRM[17]等；2)從通用的軟件工程領(lǐng)域產(chǎn)生的軟件需求規(guī)約方法，如：統(tǒng)一建模語言(UML)[18]中的用例(UseCase)模型[19]的需求捕獲與描述方法、從UML擴(kuò)展而來的系統(tǒng)建模語言(SysML)中用于描述系統(tǒng)需求的參數(shù)模型，其典型工具包括了：Raphsody，Statmate[20]等；3)從電子硬件系統(tǒng)設(shè)計(jì)的同步數(shù)據(jù)流語言發(fā)展而來的需求建模與代碼生成技術(shù)，如：MATLAB公司的Simulink工具[21]、基于Esterel技術(shù)的SCADE工具等；最后一類是以自然語言或者采用限定結(jié)構(gòu)的自然語言來描述系統(tǒng)和軟件需求[22].

相比較而言，統(tǒng)一建模語言UML/SysML所提供的圖形化符號在完整性、一致性和數(shù)學(xué)的嚴(yán)謹(jǐn)性上強(qiáng)調(diào)的不夠.僅使用UML/SysML提供的需求描述方法不足以滿足現(xiàn)代安全關(guān)鍵航電系統(tǒng)和軟件的需求設(shè)計(jì)、分析和驗(yàn)證的要求.而基于同步數(shù)據(jù)流的圖形化建模語言(如：Simulink和SCADE)設(shè)計(jì)初衷為系統(tǒng)和軟件的設(shè)計(jì)，近些年被應(yīng)用于建模需求規(guī)范.但從DO-178C中要求的多層級需求來看，Simulink和SCADE描述的需求模型最多屬于DO-178C中的低級需求.其原因是：在這些模型中通常都包含了很明顯的設(shè)計(jì)信息和細(xì)節(jié).最后一類限定自然語言的需求方法(如：RSL[23]采用限定的結(jié)構(gòu)化的自然語言描述需求)，通常使用DOORS對條目化需求進(jìn)行管理.但DOORS本身只是一個(gè)需求管理工具，并不能對需求的語義進(jìn)行檢查.因此，當(dāng)系統(tǒng)的規(guī)模增大，所構(gòu)造的大量需求條目必不可少存在二義性、完整性等問題，顯然DOORS工具無法支撐DO-178C任何一個(gè)層級的需求分析和驗(yàn)證的任務(wù)要求.

本文提出了一種面向領(lǐng)域自然語言需求的模板化規(guī)約方法，通過嚴(yán)格定義數(shù)學(xué)語義的領(lǐng)域概念庫和領(lǐng)域模板庫，對條目化的自然語言需求進(jìn)行規(guī)約，以減少其二義性.其次，給出了從規(guī)范化需求模型到VRM模型的自動轉(zhuǎn)換，包括領(lǐng)域概念庫到數(shù)據(jù)字典的轉(zhuǎn)換規(guī)則以及領(lǐng)域模板庫到行為表的轉(zhuǎn)換規(guī)則.最后，在.net平臺上實(shí)現(xiàn)了原型工具，并基于實(shí)際工業(yè)案例EICAS系統(tǒng)進(jìn)行了案例分析.

在未來的工作中，在領(lǐng)域概念庫方面，對已有的一些實(shí)例進(jìn)行領(lǐng)域概念庫的構(gòu)建，以方便工程人員的使用.在領(lǐng)域模板庫方面，為了更加貼合實(shí)際的工程需求，進(jìn)一步改進(jìn)和擴(kuò)充領(lǐng)域模板，使其更加貼合實(shí)際使用的目標(biāo)工程.VRM模型構(gòu)建完成后，進(jìn)行模型的自動化分析，(如：一致性、完整性的檢查)，模型元素信息的追蹤設(shè)計(jì)以及測試用例的自動生成等工作.