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

1(南京航空航天大學 計算機科學與技術學院，南京 211106)

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

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

1 引 言

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

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

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

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

2 相關技術背景

2.1 航空認證標準DO-178B/C

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

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

2.2 基于模型的分析與驗證

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

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

3 面向領域自然語言需求的VRM建模

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

3.1 面向領域自然語言建模的框架

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

圖1 航電軟件需求工具ART

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

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

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

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

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

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

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

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

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

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

3.2 VRM建模

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

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

VRM需求規(guī)約的六元組：{SV，C，E，F(xiàn)，TS，VR}.其中SV是所有狀態(tài)變量的集合，為一個四元組，定義為：SV={MV，CV，M，IV}，包含輸入變量MV、輸出變量CV、模式集M，中間變量IV.下面具體介紹六元組每個數(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為某個模式集，它包含了該模式集下的所有模式，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中的某個變量，TS 是r的值域類型.VR(r)是r可能取值的集合.

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

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

EVENT(S)GUARDD.

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

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

在VRM模型中，表格函數(shù)包括3大類：條件表，事件表和模式轉換表.這3類表都有相應的形式化語義定義.限于篇幅，以下僅以示例1和示例2給出簡要概述.示例1是一個條件表的例子，語義為：基于狀態(tài)依賴關系Dn={Pressure，Overriden}定義了輸出變量SafetyInjection的取值情況(即某個功能需求F1).其對應的二維表用于直觀表示數(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則給出一個事件表的例子，是基于新舊狀態(tài)依賴關系集合：{Block，Reset，Pressure，Overriden}和{Block，Reset，Pressure}，函數(shù)定義了輸出變量Overridden的值(即某個功能需求F2).其對應的二維表用于直觀表示數(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é)研究框架中所涉及到的關鍵概念，進行詳細的設計定義.首先，介紹了使用N元組的形式定義領域概念庫中的具體內(nèi)容；其次，表述了領域模板庫的具體內(nèi)容，以及其組成元素的數(shù)學定義；最后描述了VRM模型自動構造的算法及其說明.

4.1 領域概念庫

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

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

本文采取面向對象中類定義的思想對領域概念庫中的內(nèi)容進行定義，如圖3所示，并采用N元組的形式進行表示(見表3).

表3 領域概念庫語義定義

圖3 領域概念庫層級關系

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

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

表4 需求示例領域概念庫

4.2 領域模板庫

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

4.2.1 領域模板

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

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

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

3)顯示條件：當滿足以下條件，<對象>應能夠<功能><格式/要求/標準>：<條件>.

4)顯示事件：當發(fā)生以下事件，<對象>應能夠<功能><格式/要求/標準>：<事件>.

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

下面以顯示條件模板進行舉例說明.例如4.1節(jié)中的示例，“opFADECEngineThrustReferenceGraphicColor”對應于<對象>，“Green 100”對應于<格式/要求/標準>，“顯示”對應于<功能>，“ipFADECEngineManualThrottleCmd等于true時”對應于<條件>.

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

4.2.2 條件模板

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

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

ci=(O，R，V)

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

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

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

因此，條件模板采用如下的BNF范式進行定義.c表示簡單條件，C_term表示組成條件的項，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 事件模板

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

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

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

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

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

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

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

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

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

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

表5 事件模板

4.3 模型構造

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

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

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

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

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

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

4.3.2 VRM模型

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

圖5 VRM模型數(shù)據(jù)結構

4.3.3 VRM模型構造

VRM模型構造分為3種類型：

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

算法1.生成常量字典

輸入：ConceptConst

輸出：DictionaryConst

1.foreach ConceptConst cc in arrayConceptConstdo

2. DictionaryConstDataValue = cc.getValue()；

3. dc.setDictionaryConst()；

4. arrayDC.add(dc)；

5.endfor；

常量字典構造算法的輸入為常量領域概念，輸出為常量字典.單個的常量使用4.3.2章節(jié)中定義的常量字典類的實例化對象進行存儲，常量字典則為常量對象所組成的常量對象數(shù)組.通過對常量領域概念對象數(shù)組進行遍歷，將其中所包含的常量字典語義信息進行轉換.因為只進行了一次循環(huán)，故算法復雜度為O(n).

2)行為表：輸出變量(中間變量)條件表和輸出變量(中間變量)事件表的構造.構造算法見算法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

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

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

3)模式轉換表的構造.構造算法見算法3.

算法3.生成模式轉換表

輸入：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

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

算法的主要處理過程是先對模式集領域概念進行遍歷，獲取模式轉換表中模式集的相關信息.因為一個模式集中包含多個模式，所以對模式領域概念進行遍歷，獲取其中屬于當前模式集的相關模式，構成模式對象數(shù)組.同時，當前模式集下的模式之間的轉換可能存在多個，所以對模式轉換領域概念進行遍歷，獲取屬于當前模式集的模式轉換數(shù)據(jù)構成模式轉換對象數(shù)組.最終形成模式轉換表對象數(shù)組.因為進行了兩層循環(huán)，所以算法復雜度為O(n2).

5 EICAS實例分析

5.1 EICAS系統(tǒng)概述

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

5.2 EICAS VRM模型生成

考慮到文本篇幅，此處選取實際需求中的一部分需求進行模型的構建及模型的轉換工作實例分析.

自然語言原始需求條目.

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

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

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

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

表6 輸入變量領域概念

表7 輸出變量領域概念

表8 中間變量領域概念

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

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

1)當滿足以下條件，opFDUConfigurationFormat應能夠設置為METRIC：ipFDUConfigurationIsMetric = TRUE AND ipFDUConfigurationIsMetricStatus = Valid.

2)當滿足以下條件，opFDUConfigurationFormat應能夠設置為IMPERIAL：ipFDUConfigurationIsMetric = FALSE AND ipFDUConfigurationIsMetricStatus = Valid.

3)當滿足以下條件，opFDUConfigurationFormat應能夠設置為IMPERIAL：ipFDUConfigurationIsMetric = FALSE AND ipFDUConfigurationIsMetricStatus = Invalid.

4)當滿足以下條件，opFDUConfigurationFormat應能夠設置為IMPERIAL：ipFDUConfigurationIsMetric = TRUE AND ipFDUConfigurationIsMetricStatus = Invalid.

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

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

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

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

圖6 VRM模型

6 相關工作與小結

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

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

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

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