面向駕駛艙顯示系統需求的形式化建模與分析

戰蕓嬌，魏 歐，胡 軍，王立松，谷青范

(1.南京航空航天大學 計算機科學與技術學院，江蘇 南京 211106;2.中國航空無線電電子研究所，上海 200000)

1 概 述

需求分析是軟件開發流程中的第一步，也是最重要的一步。在航空航天領域等實際的安全關鍵系統中，由于需求的復雜性、缺乏統一的需求模型、需求描述的結構混亂和語言歧義等原因[1]，往往造成需求中存在大量的不一致和不完備。相關研究表明，在系統維護階段修改所發現的需求錯誤所需要的工作量，大約是更改需求分析階段發現的錯誤所需的工作量的200倍[2]。因此，減少需求中的錯誤至關重要，不僅能夠保證系統的安全性，也可以減少系統開發的成本。

駕駛艙顯示系統[3](cockpit display system)是駕駛員和飛機進行信息交互重要的機載系統。通過將傳統的飛行儀表信息進行數字化綜合處理，駕駛艙顯示系統采用多種顯示器按需展現各種不同數據，如主飛行顯示器、導航顯示器等，增強了駕駛員的態勢感知能力，簡化了對飛機的操縱導航，使得駕駛員能夠專注于最為相關的信息，降低飛行成本。

機載軟件[4-5]通常都具有規模龐大，數據關聯復雜，安全級別要求高等特點。其需求存在可維護性差，相同操作描述不一致，不可驗證信息較多和低層次與高層次需求不平衡等問題。在顯示系統廣泛應用的同時，在實際中也時常發生由于顯示系統錯誤而引起的安全事故。例如，2005年8月1日，馬來西亞航空公司的一架波音777-200ER從珀斯飛回吉隆坡，期間主飛行顯示器(PFD)的速度顯示區域發生顯示了飛機同時接近高速極限值和低速極限值的沖突信息，致使飛行員立即解除自動駕駛并緊急降落在珀斯[6]。這些事故都造成了生命、財產等的重大損失，影響巨大。對于駕駛艙顯示系統而言，為保障駕駛員能夠對飛機飛行中的狀況做出正確的判斷、避免事故的發生，在開發早期發現需求中存在的錯誤，可以減少需求錯誤對系統造成的影響，提高系統的安全性。因此，對駕駛艙顯示系統的需求進行嚴格的定義和分析以及錯誤檢測顯得尤為重要。

針對駕駛艙顯示系統這樣特定應用的系統需求，需要判定其是否滿足一致性和完備性。從廣義上來說，一致性保證需求中不存在矛盾的信息，完備性保證需求中必須包含那些對于系統正常工作、保證系統安全所必要的信息。因此，應檢測需求中是否存在以下問題：

(1)檢測出需求中未定義的顯示情況，即完備性問題。目的是避免顯示器上出現需求中沒有定義的某種顯示信息。

(2)檢測出需求中出現的顯示不確定性問題，即一致性問題。目的是避免顯示器上出現矛盾的信息顯示。

(3)檢測出需求中缺失的并且影響系統安全的信息，如數據的時間邊界、數據的有效性等。

T-VEC工具是對復雜系統的需求階段進行錯誤檢測與驗證，并對設計階段進行仿真的工具。1989年以來，其廣泛應用在飛機領域的安全關鍵性系統、實時系統和許多嵌入式系統中。文中主要利用T-VEC的測試向量生成工具，對表格式需求進行測試驗證。通過對變量和條件等相關需求模型的輸入，對需求進行編譯，以檢測需求中的各種錯誤和特性。

針對以上問題，為了找到駕駛艙顯示系統這樣的安全關鍵系統需求中的錯誤，就需要一套完整的方法來對需求進行一致性和完備性檢測工作。文中以四變量模型為基礎，提出了具體的建立駕駛艙顯示系統的需求模型的方法，包括對需求描述方式和嚴格的語義，支持需求的一致性和完備性的T-VEC檢測工具。

2 四變量模型

四變量模型[7-9](four-variable model)是由Parnas提出來的用以指明需求的方法，如圖1所示。

圖1 四變量模型

四變量模型中的變量是時間連續型函數，分為四類變量：

(1)監督變量(monitored variables，MON)：系統需要觀測的外部環境量；

(2)受控變量(controlled variables，CON)：受系統控制的環境量；

(3)輸入變量(input variables，INPUT)：由傳感器等輸入設備將監督變量轉換而來的變量；

(4)輸出變量(output variables，OUTPUT)：發送到輸出設備上的、改變受控變量的變量。

例如，監督變量可以是飛機在飛行中的飛行高度和飛行速度，受控變量可以是顯示儀表盤上飛行高度和飛行速度值的顯示；相應的輸入輸出變量可以是軟件讀入的、寫出的ARINC-429總線上的數據。

在這些變量上，定義了4種數學關系：

(1)NAT：施加在環境量上的自然限制，例如飛機的最大爬升率；

(2)REQ：定義了系統需求，指明受控變量與監督變量的關系。系統需求REQ是可行的，當且僅當REQ中考慮了NAT中的所有環境限制條件。

(3)IN：描述了監督變量和輸入變量之間的關系。IN模擬了輸入硬件接口，如傳感器和模數轉化器；

(4)OUT：描述輸出變量和受控變量之間的關系。OUT模擬了輸出硬件接口，如數模轉換器和作動器。

3 駕駛艙顯示系統的需求模型

結合駕駛艙顯示系統的特點，利用四變量模型框架找出需求中的變量和關系，再利用表格符號的形式將需求中的關系表示出來，建立需求模型。

3.1 需求的組成

對系統進行準確的描述從而形成需求，意味著需要確定系統、子系統和組件的行為(并無必要知道行為是如何具體實現的)。Parnas最初提出的四變量模型是用來準確描述系統需求、并形成相應需求文檔的方法。

針對駕駛艙顯示系統中輸入變量對顯示信息的影響——一組輸入變量取值情況對同一顯示造成的影響不同，且這些變量之間存在依賴關系，對輸入變量進行分類。在駕駛艙顯示系統上所顯示的信息包括兩類：一類是數值、文本或圖形信息，另一類是數值、文本或圖形的樣式信息(如顏色和字體)。將駕駛艙顯示系統需求的輸入變量分為顯性變量(explicit variables)和隱性變量(implicit variables)。顯性變量：參數(輸入變量)的值直接決定了顯示器上數值、文本或圖形信息的顯示；隱性變量：參數的值僅僅影響數值、文本或圖形的顯示樣式。其中，顯性變量和隱性變量對系統安全造成的影響有所不同，顯性變量失效直接造成顯示器上相關區域的讀數/文本、圖形信息為空，飛行員無法從顯示器上得知任何有關飛機的狀態信息，而隱性變量僅僅影響了顯示器上顯示信息的樣式；隱性變量在顯示器上的顯示依賴于顯性變量的有效性/取值情況，只有在顯性變量有效且取特定值情況下，隱性變量的取值情況才會對顯示信息造成影響。

另外，為了更好地利用四變量模型準確描述駕駛艙顯示系統需求，以便用表格符號對需求中的關系進行表示，需要提供兩種額外的結構：條件(condition)和事件(events)。條件是定義在系統輸入和輸出上的謂詞；當兩個或多個隱性變量之間的大小關系發生變化，就表示一個事件發生。

圖2是結合顯示系統的體系結構[10]，參考四變量模型，描述駕駛艙顯示系統需求的結構概念圖。其中，傳感器(sensor)采集外部環境的監督變量(monitor variables)，將其轉換成系統可識別的輸入變量，并傳遞給顯示系統控制單元；子系統(subsystem)采集來自系統內部的監督變量—飛機系統自身的狀態信息，如：FADEC采集引擎參數和控制引擎，通過轉換傳遞給顯示系統控制單元；cockpit display controller unit表示處理從傳感器和其他子系統傳遞而來的參數的處理單元，一方面，它將處理后的顯示信息指令傳遞給顯示單元，另一方面，將產生的指令反饋給自身(如圖中黑色箭頭所示)，作為系統內部其他功能的控制條件；cockpit display unit表示顯示單元，接收來自處理單元處理后產生的顯示信息指令，并在顯示器上給予特定的顯示。

圖2 駕駛艙顯示系統需求結構概念圖

3.2 需求的表格符號表示

系統開發工程師發現：利用表格表示需求[11]，不僅有利于開發人員對系統的理解和開發，還能將大量的需求信息準確地表示出來[12]。因此，在利用四變量模型找出系統需求中存在的各個組件和變量的基礎上，利用表格符號[13]來表示需求中變量之間的關系。鑒于駕駛艙顯示系統內部各個組件的功能不同，分別定義不同的表格予以表示：對于傳感器和子系統，這兩種組件都是將監督變量(來自內部環境和外部環境)轉換成顯示系統控制單元可識別的量，因此，定義輸入映射表(mapping table of input)作為監督變量和輸入變量的對應關系；對于顯示單元，它接收來自顯示控制單元的輸出變量(顯示指令)，并控制顯示單元的受控變量的顯示，因此，定義輸出映射表(mapping table of output)作為輸出變量和受控變量的對應關系；對于駕駛艙顯示系統控制單元到顯示單元的特殊性—在不同的顯示邏輯下，將從傳感器和其他子系統傳遞而來的參數，在顯示單元上予以相應的顯示—定義三種表格：映射表(mapping table)、事件表(event table)和條件表(condition table)。這三種表格都對應了四變量模型中的SOF，而且，這里的顯示控制單元的輸出變量是與受控變量有關的，每一個表格中的輸出變量(輸出變量組)都唯一對應一個受控變量。映射表：與受控變量相關的輸出變量的取值情況由輸入變量的取值情況確定；事件表：與受控變量相關的輸出變量的取值情況取決于輸入變量的取值情況和所發生的事件；條件表：與受控變量相關的輸出變量的取值情況取決于輸入變量的取值情況和當前的條件。除此之外，還需要定義輸入變量表格(input table)和輸出變量表格(output table)，確定輸入和輸出變量的類型、取值范圍，不僅有利于查看系統中所有的輸入和輸出變量，還方便后續對需求的一致性和完備性檢測工作。

4 需求模型的語義

上一節，通過參考四變量模型，利用表格符號，將用自然語言描述的需求轉換成表格符號表示的需求，建立需求模型。接下來，需要為需求模型提供精確的語義[14]。這里的需求模型，對于SOF，定義了輸出根據輸入或者輸入、條件(事件)的改變而發生的變化；描述了從表格中導出的表格函數(table function)—表格符號的形式化表示。這些表格函數不僅定義了從輸入到輸出或者輸入、條件(事件)到輸出的映射關系，還定義了監督變量和輸入變量、輸出變量和受控變量的映射關系。定義一個七元組(MV,CV,D,C,E,F,VS)來表示該需求模型，其中D表示數據項，包含輸入和輸出變量，D={IP,OP}，輸入變量分為顯性變量和隱性變量，即IP={EX_IP,IM_IP}。

為了闡述形式化模型，有關元組的定義如下：

(1)七元組元素：模型中的監督變量、輸入、輸出和受控變量，以及條件、事件、輸入輸出的取值范圍。定義以下集合：

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

CV：非空的不相交的受控變量集合，CV={cv1,cv2,…,cvk}，cv1,cv2,…,cvk稱為受控變量；

IP：非空的不相交的輸入變量集合，IP={ip1,ip2,…,ipl}，ip1,ip2,…,ipl稱為輸入；

OP：非空的不相交的輸出變量集合，OP={op1,op2,…,opm}，op1,op2,…,opm稱為輸出；

VS：表示輸入輸出變量的所有取值范圍。假設r代表輸入或者輸出變量，那么其取值范圍為VS(r)；

C：條件，條件是定義在輸入或輸出上的謂詞。條件，如真、假或者邏輯表達式r⊙r'或r⊙a，其中r,r'表示輸入、輸出變量，a表示常數值，⊙∈{=,<,>,≠,>=,<=}表示關系操作符；

F：系統功能，在第3節中，所有的組件的功能都可以用表格表示，這些表格都描述成表格函數fi。

(2)輸入映射表：該表格描述了所有的監督變量到所有的輸入變量的映射關系fMI:MV→IP，準確地定義ρMI={(mvi,ipi)∈MV×IP},i=1,2,…,n，ρMI必須滿足：

(a)對于任意的監督變量都存在唯一(?!)的輸入變量與其對應，?mvi?!ipi:ipi=fMI(mvi)；

(b)對于任意的輸入變量只存在唯一的監督變量與其對應。

(3)輸出映射表：該表格描述了所有的輸出變量到所有的受控變量的映射關系fOC:OP→CV，準確地定義ρOC={((opi,…,opj),cvi)∈OP×CV};i,j=1,2,…,n，關系ρOC必須滿足：

(a)對于任意的輸出變量都存在唯一(?!)的受控變量與其對應，?opi?!cvi:cvi=fMI(opi)；

(b)同一個受控變量可能對應多個輸出變量。

(4)受控變量CV映射表：在輸入變量取值不同情況下，相對應的輸出變量取值情況。準確地定義ρi={(∪IPi,k,∪OPi,k)∈∪VS(IPi)×∪VS(OPi)},k=1,2,…,n。其中∪VS(IPi)作為與受控變量cv相關的所有輸入組成的輸入變量組取值情況的集合，∪VS(OPi)作為與cv相關的所有輸出組成的輸出變量組取值情況的集合，IPi,k表示單個輸入變量IPi的取值。關系ρi必須滿足以下屬性：

為了明確具體的輸出和輸入之間的關系，用表格函數fi替換關系ρi，其中屬性(a)、(b)、(c)保證了fi是一個函數，屬性(c)、(d)保證了fi是雙射：

(1)

(5)受控變量CV條件表：在輸入變量取值不同的情況下，輸出變量的取值情況。準確地定義ρi={((∪IPi,k,ci,j),∪OPi,k)∈(∪VS(IPi)×{Ci,1,Ci,2})×∪VS(OPi)},k=1,2,…,n;j=1,2。其中Ci是與受控變量相關的條件，ci,j表示保證條件Ci的真假情況。關系ρi必須滿足以下屬性：

(d)表格中，在所有輸入變量取值確定的情況下，其對應的條件Ci的所有取值情況ci,j都包含在表格內，因為Ci只可以取布爾值，所以對于任意的i:ci,1=T∧ci,2=F；

用表格函數fi替換關系ρi，其中屬性(a)、(c)、(d)、(e)保證fi是一個函數，屬性(b)、(c)保證fi是雙射：

OPi=fi(IPi,Ci)=

(2)

(6)受控變量CV事件表：在發生事件的情況下，輸入變量取值如何影響與受控變量相關的輸出變量的取值。由于事件表同條件表類似，只是將條件替換為事件，因此不再贅述。

5 案例分析

引擎指示和機組警告系統[15](engine-indicating and crew-alerting system,EICAS)是為飛機機組顯示提供飛機引擎和其他系統運轉情況的綜合顯示系統。

EICAS通常包含多種引擎參數顯示儀表，如引擎轉速、引擎溫度、燃料流速和燃料量、油壓等。被EICAS系統監督的其他飛機系統包括液壓、氣動、電力、除冰系統、飛行操作系統等。EICAS是駕駛艙顯示系統的重要組成部分，以軟件驅動的電子系統取代了原有的模擬儀表裝置，其大部分顯示區域用作導航和定位顯示。機組警告系統(CAS)用來取代舊式系統中的信號指示面板，CAS不再單單以亮起指示燈來顯示系統故障，而是在EICAS的指示區域顯示一系列的信息來告知機組人員系統故障。

表1是駕駛艙顯示系統中EICAS需求的一部分(由于篇幅原因，并沒有將完整的需求文檔內容進行展示，展示的是用表格符號表示后的需求)。它是關于引擎推力模式顯示的條件表：在飛機飛行的不同階段，飛機引擎的推力模式不同，EICAS系統通過接收從其他相關子系統傳遞來的參數，根據參數的取值情況確定并顯示當前引擎推力的模式。其中，ipFADECEngineNormalTOSelected代表引擎正常全推力起飛模式是否被選中的參數，當參數取值為True時代表被選中(下同)；ipFADECEngineFlexTOSelected代表非全推力起飛模式是否被選中的參數；ipFADECEngine-NormalCLBSelected代表飛機是否處于全推力爬升模式的參數；ipFADECEngineCruiseSelected代表飛機引擎是否以巡航模式運作的參數；ipFADECEngineGASelected代表飛機引擎是否以復飛模式運作的參數；ipFADECEngineMCTSelected代表飛機引擎是否以最大連續推力模式運作的參數；ipFADECEngineTO1DerateSelected代表飛機是否以減推力模式1起飛的參數；ipFADECEngineTO2DerateSelected代表飛機是否以減推力模式2起飛的參數；條件Reduced thrusttakeoff代表減推力起飛模式是否被選擇；輸出項的模式文本顯示opText_cvThrustMode取值：TO(正常全推力起飛)、FLEX-TO(非全推力起飛)、D-TO1(減推力模式1起飛)、D-TO2(減推力模式2起飛)、CLB(全推力爬升模式)、CON(連續最大推力飛行模式)、CRZ(巡航模式)、G/A(復飛模式)，opFont_cvThrustMode為輸出模式文本的字體，opColor_cvThrustMode為輸出模式文本的顏色。

表1 引擎推力模式cvThrustMode條件表

該條件表所表示的函數如下所示：

(opi,cvi)=fi(ip1,ip2,…,ip8,ci)=

(3)

其中，ip1,ip2,…,ip8表示輸入變量；RTT表示條件Reduced Thrust Takeoff；op1,op2,op3表示輸出變量。

6 結束語

需求的一致性和完備性對于系統的安全性起著至關重要的作用。找出需求中存在的錯誤，避免其對系統造成的不良影響，可以提高系統的安全性。傳統的人工方法對需求進行檢查和評審，不僅費時費力，而且容易忽略需求中存在的錯誤。利用Parnas提出的四變量模型作為指導框架確定駕駛艙顯示系統的需求組成和關系，并用表格符號將需求進行表示，建立需求模型；運用形式化方法為需求模型定義精確的語義，并利用T-VEC工具進行檢測。通過這一系列的工作，不僅可以準確地描述需求，而且找出了需求中存在的錯誤。

在將來的工作中，計劃開發出一個支持T-VEC工具到符號化模型檢測語言NuSMV的自動化工具，支持需求的安全性檢測，找出需求中存在的安全錯誤，從而產生高質量的需求。這樣的高質量需求，可以減少需求錯誤對系統的影響，提高系統的安全性。同時，自動化工具也減少了系統開發的成本。

[1] VERAS P C,VILLANI E,AMBROSIO A M,et al.Errors on space software requirements:a field study and application scenarios[C]//IEEE international symposium on software reliability engineering.[s.l.]:IEEE,2010.

[2] BOEHM B W. Software engineering economics[J].IEEE Transactions on Software Engineering,1984,10(1):4-21.

[3] ZHOU Y,ZHUANG D,ZHANG L,et al.Study on ergonomics evaluation method of the cockpit display system[C]//IEEE international conference on computer-aided industrial design & conceptual design.[s.l.]:IEEE,2010.

[4] GALLOWAY A,IWU F,MCDERMID J,et al.On the formal development of safety-critical software[M]//Verified software:theories,tools,experiments.Berlin:Springer-Verlag,2005:362-373.

[5] 陳 鑫，王 輝，牟 明.滿足DO-178B要求的軟件需求開發方法[J].計算機工程與設計,2012,33(7):2673-2677.

[6] 陳光穎，黃志球，陳 哲，等.面向DO-333的襟縫翼控制單元安全性分析[J].計算機科學，2016，43(5)：150-156.

[7] PARNAS D L,MADEY J.Functional documents for computer systems[J].Science of Computer Programming,1995,25(1):41-61.

[8] PARNAS D L.From requirements to architecture[C]//New

trends in software methodologies,tools and techniques.[s.l.]:IOS Press,2010:3-36.

[9] LEVESON N G,HEIMDAHL M P E,HILDRETH H,et al.Requirements specification for process-control systems[J].IEEE Transactions on Software Engineering,1994,20(9):684-707.

[10] MOIR I,SEABRIDGE A,JUKES M.Civil avionics systems[M].[s.l.]:John Wiley & Sons,2013.

[11] PARNAS D L.Tabular representation of relations[D].Canada:Telecommunications Research Institute of Ontario McMaster University,1997.

[12] HEITMEYER C L,JEFFORDS R D,LABAW B G.Automated consistency checking of requirements specifications[J].ACM Transactions on Software Engineering & Methodology,1996,5(3):231-261.

[13] 張 鵬，劉 磊，劉華虓，等.Tabular表達式的指稱語義研究[J].軟件學報,2014,25(6):1212-1224.

[14] HATTON L.What is a formal method (and what is an informal method)?[C]//Proceedings of the 12th annual conference on computer assurance 1997.[s.l.]:IEEE,1997:125-126.

[15] WELLS A T,RODRIGUES C C.Commercial aviation safety[M].[s.l.]:McGraw-Hill Professional,2011.