增強(qiáng)飛行視景系統(tǒng)作為飛機(jī)上的復(fù)雜電子系統(tǒng),傳統(tǒng)的安全性分析面臨工作量大,過(guò)于依賴(lài)分析人員經(jīng)驗(yàn),容易出錯(cuò)等問(wèn)題,Petri網(wǎng)、概率模型等形式化方法雖然提高了分析的自動(dòng)化水平,減少了一定的分析工作量,但也面臨不能自上而下進(jìn)行安全性需求分配的問(wèn)題。為解決上述問(wèn)題,提出了基于模型檢驗(yàn)的形式化安全性分析方法。實(shí)現(xiàn)對(duì)增強(qiáng)飛行視景系統(tǒng)的定性、定量安全性分析,提高分析效率。研究包括以下幾個(gè)方面:(1)首先,通過(guò)對(duì)該系統(tǒng)的架構(gòu)和數(shù)據(jù)流進(jìn)行抽象,分模塊級(jí)、LRU級(jí)、系統(tǒng)級(jí)三層,建立了系統(tǒng)的形式化名義模型,并進(jìn)行了驗(yàn)證。(2)研究模型擴(kuò)展方法,編寫(xiě)故障庫(kù)模板,將底層模塊的故障模式注入到名義模型,建立形式化擴(kuò)展模型。(3)將典型失效狀態(tài)用形式化規(guī)約描述,進(jìn)行自動(dòng)計(jì)算,得到故障樹(shù)最小割集,基于該最小割集進(jìn)行了定性和定量分析,其中在定量分析,提出一種安全性分配方法,并實(shí)現(xiàn)了自動(dòng)分配工具。結(jié)果表明,該方法自動(dòng)化程度高,且解決了其它形式化方法如Petri網(wǎng)、概率模型等無(wú)法進(jìn)行自上而下概率分配的問(wèn)題,能夠更加有效地促進(jìn)系統(tǒng)設(shè)計(jì)階段的安全性工作。

【文章頁(yè)數(shù)】：97 頁(yè)

【學(xué)位級(jí)別】：碩士

【部分圖文】：

圖2-4模型檢驗(yàn)示意

中國(guó)民航大學(xué)碩士學(xué)位論文12圖2-4模型檢驗(yàn)示意模型檢驗(yàn)中的系統(tǒng)模型用Kripke結(jié)構(gòu)表示。其由一個(gè)五元組MS,S0,AP,R,L=構(gòu)成，其中S表示有限狀態(tài)集合，0S是初始狀態(tài)集合，且0S是S的子集，AP表示由原子命題及和它們的非構(gòu)成的集合，R表示狀態(tài)轉(zhuǎn)移關(guān)系，映射L:S→2|A....

圖3-1低能見(jiàn)度情況下飛行員裸眼

中國(guó)民航大學(xué)碩士學(xué)位論文16第三章EFVS系統(tǒng)形式化名義模型建模3.1建模范圍模型是對(duì)事物的抽象，用嚴(yán)謹(jǐn)?shù)恼Z(yǔ)言來(lái)定義，模型是要素與要素之間聯(lián)系的集合。因此在不同的情境中，模型的含意有所不同。比如，玻璃柜臺(tái)中擺放的靜態(tài)飛機(jī)模型，和航空愛(ài)好者制作的可以飛行的航模。二者都是模型，卻有很....

圖3-7非均勻校正模塊RSML-e模型

中國(guó)民航大學(xué)碩士學(xué)位論文23圖3-7非均勻校正模塊RSML-e模型RSML-e模型的上半部分是數(shù)據(jù)定義，Image_NUCM_out表示非均勻校正模塊輸出的圖像數(shù)據(jù)；Type表示數(shù)據(jù)類(lèi)型為枚舉型，有normal，error，empty三個(gè)枚舉值，分別代表正常、....

圖3-8非均勻校正模塊狀態(tài)轉(zhuǎn)移條件AND-OR表

中國(guó)民航大學(xué)碩士學(xué)位論文24(（Im__）)(（__）)(（__）)ageDMouterrorTRUETRUETRUEBFDtoEVSemptyTRUETRUETRUEBFDtoEVSerror===化簡(jiǎn)的表達(dá)式為（Im....

本文編號(hào)：4027363