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

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

1 概 述

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

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

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

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

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

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

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

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

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

2 四變量模型

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

圖1 四變量模型

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

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

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

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

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

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

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

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

(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)換器和作動(dòng)器。

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

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

3.1 需求的組成

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

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

另外，為了更好地利用四變量模型準(zhǔn)確描述駕駛艙顯示系統(tǒng)需求，以便用表格符號(hào)對(duì)需求中的關(guān)系進(jìn)行表示，需要提供兩種額外的結(jié)構(gòu)：條件(condition)和事件(events)。條件是定義在系統(tǒng)輸入和輸出上的謂詞；當(dāng)兩個(gè)或多個(gè)隱性變量之間的大小關(guān)系發(fā)生變化，就表示一個(gè)事件發(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)可識(shí)別的輸入變量，并傳遞給顯示系統(tǒng)控制單元；子系統(tǒng)(subsystem)采集來(lái)自系統(tǒng)內(nèi)部的監(jiān)督變量—飛機(jī)系統(tǒng)自身的狀態(tài)信息，如：FADEC采集引擎參數(shù)和控制引擎，通過(guò)轉(zhuǎn)換傳遞給顯示系統(tǒng)控制單元；cockpit display controller unit表示處理從傳感器和其他子系統(tǒng)傳遞而來(lái)的參數(shù)的處理單元，一方面，它將處理后的顯示信息指令傳遞給顯示單元，另一方面，將產(chǎn)生的指令反饋給自身(如圖中黑色箭頭所示)，作為系統(tǒng)內(nèi)部其他功能的控制條件；cockpit display unit表示顯示單元，接收來(lái)自處理單元處理后產(chǎn)生的顯示信息指令，并在顯示器上給予特定的顯示。

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

3.2 需求的表格符號(hào)表示

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

4 需求模型的語(yǔ)義

上一節(jié)，通過(guò)參考四變量模型，利用表格符號(hào)，將用自然語(yǔ)言描述的需求轉(zhuǎn)換成表格符號(hào)表示的需求，建立需求模型。接下來(lái)，需要為需求模型提供精確的語(yǔ)義[14]。這里的需求模型，對(duì)于SOF，定義了輸出根據(jù)輸入或者輸入、條件(事件)的改變而發(fā)生的變化；描述了從表格中導(dǎo)出的表格函數(shù)(table function)—表格符號(hào)的形式化表示。這些表格函數(shù)不僅定義了從輸入到輸出或者輸入、條件(事件)到輸出的映射關(guān)系，還定義了監(jiān)督變量和輸入變量、輸出變量和受控變量的映射關(guān)系。定義一個(gè)七元組(MV,CV,D,C,E,F,VS)來(lái)表示該需求模型，其中D表示數(shù)據(jù)項(xiàng)，包含輸入和輸出變量，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(bǔ)，其中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)對(duì)于任意的監(jiān)督變量都存在唯一(?!)的輸入變量與其對(duì)應(yīng)，?mvi?!ipi:ipi=fMI(mvi)；

(b)對(duì)于任意的輸入變量只存在唯一的監(jiān)督變量與其對(duì)應(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)對(duì)于任意的輸出變量都存在唯一(?!)的受控變量與其對(duì)應(yīng)，?opi?!cvi:cvi=fMI(opi)；

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

(4)受控變量CV映射表：在輸入變量取值不同情況下，相對(duì)應(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表示單個(gè)輸入變量IPi的取值。關(guān)系ρi必須滿足以下屬性：

為了明確具體的輸出和輸入之間的關(guān)系，用表格函數(shù)fi替換關(guān)系ρi，其中屬性(a)、(b)、(c)保證了fi是一個(gè)函數(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)表格中，在所有輸入變量取值確定的情況下，其對(duì)應(yīng)的條件Ci的所有取值情況ci,j都包含在表格內(nèi)，因?yàn)镃i只可以取布爾值，所以對(duì)于任意的i:ci,1=T∧ci,2=F；

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

OPi=fi(IPi,Ci)=

(2)

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

5 案例分析

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

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

表1是駕駛艙顯示系統(tǒng)中EICAS需求的一部分(由于篇幅原因，并沒(méi)有將完整的需求文檔內(nèi)容進(jìn)行展示，展示的是用表格符號(hào)表示后的需求)。它是關(guān)于引擎推力模式顯示的條件表：在飛機(jī)飛行的不同階段，飛機(jī)引擎的推力模式不同，EICAS系統(tǒng)通過(guò)接收從其他相關(guān)子系統(tǒng)傳遞來(lái)的參數(shù)，根據(jù)參數(shù)的取值情況確定并顯示當(dāng)前引擎推力的模式。其中，ipFADECEngineNormalTOSelected代表引擎正常全推力起飛模式是否被選中的參數(shù)，當(dāng)參數(shù)取值為True時(shí)代表被選中(下同)；ipFADECEngineFlexTOSelected代表非全推力起飛模式是否被選中的參數(shù)；ipFADECEngine-NormalCLBSelected代表飛機(jī)是否處于全推力爬升模式的參數(shù)；ipFADECEngineCruiseSelected代表飛機(jī)引擎是否以巡航模式運(yùn)作的參數(shù)；ipFADECEngineGASelected代表飛機(jī)引擎是否以復(fù)飛模式運(yùn)作的參數(shù)；ipFADECEngineMCTSelected代表飛機(jī)引擎是否以最大連續(xù)推力模式運(yùn)作的參數(shù)；ipFADECEngineTO1DerateSelected代表飛機(jī)是否以減推力模式1起飛的參數(shù)；ipFADECEngineTO2DerateSelected代表飛機(jī)是否以減推力模式2起飛的參數(shù)；條件Reduced thrusttakeoff代表減推力起飛模式是否被選擇；輸出項(xiàng)的模式文本顯示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é)束語(yǔ)

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

在將來(lái)的工作中，計(jì)劃開(kāi)發(fā)出一個(gè)支持T-VEC工具到符號(hào)化模型檢測(cè)語(yǔ)言NuSMV的自動(dòng)化工具，支持需求的安全性檢測(cè)，找出需求中存在的安全錯(cuò)誤，從而產(chǎn)生高質(zhì)量的需求。這樣的高質(zhì)量需求，可以減少需求錯(cuò)誤對(duì)系統(tǒng)的影響，提高系統(tǒng)的安全性。同時(shí)，自動(dòng)化工具也減少了系統(tǒng)開(kāi)發(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要求的軟件需求開(kāi)發(fā)方法[J].計(jì)算機(jī)工程與設(shè)計(jì),2012,33(7):2673-2677.

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