戰(zhàn)蕓嬌，魏 歐，胡 軍，王立松，谷青范

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

1 概 述

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

駕駛艙顯示系統(tǒng)[3](cockpit display system)是駕駛員和飛機進(jìn)行信息交互重要的機載系統(tǒng)。通過將傳統(tǒng)的飛行儀表信息進(jìn)行數(shù)字化綜合處理，駕駛艙顯示系統(tǒng)采用多種顯示器按需展現(xiàn)各種不同數(shù)據(jù)，如主飛行顯示器、導(dǎo)航顯示器等，增強了駕駛員的態(tài)勢感知能力，簡化了對飛機的操縱導(dǎo)航，使得駕駛員能夠?qū)Ｗ⒂谧顬橄嚓P(guān)的信息，降低飛行成本。

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

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

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

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

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

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

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

2 四變量模型

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

圖1 四變量模型

四變量模型中的變量是時間連續(xù)型函數(shù)，分為四類變量：

(1)監(jiān)督變量(monitored variables，MON)：系統(tǒng)需要觀測的外部環(huán)境量；

(2)受控變量(controlled variables，CON)：受系統(tǒng)控制的環(huán)境量；

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

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

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

在這些變量上，定義了4種數(shù)學(xué)關(guān)系：

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

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

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

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

3 駕駛艙顯示系統(tǒng)的需求模型

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

3.1 需求的組成

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

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

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

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

圖2 駕駛艙顯示系統(tǒng)需求結(jié)構(gòu)概念圖

3.2 需求的表格符號表示

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

4 需求模型的語義

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

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

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

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

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：表示輸入輸出變量的所有取值范圍。假設(shè)r代表輸入或者輸出變量，那么其取值范圍為VS(r)；

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

F：系統(tǒng)功能，在第3節(jié)中，所有的組件的功能都可以用表格表示，這些表格都描述成表格函數(shù)fi。

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

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

(b)對于任意的輸入變量只存在唯一的監(jiān)督變量與其對應(yīng)。

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

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

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

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

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

(1)

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

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

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

OPi=fi(IPi,Ci)=

(2)

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

5 案例分析

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

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

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

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

該條件表所表示的函數(shù)如下所示：

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

(3)

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

6 結(jié)束語

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

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

[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要求的軟件需求開發(fā)方法[J].計算機工程與設(shè)計,2012,33(7):2673-2677.

[6] 陳光穎，黃志球，陳 哲，等.面向DO-333的襟縫翼控制單元安全性分析[J].計算機科學(xué)，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表達(dá)式的指稱語義研究[J].軟件學(xué)報,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.