現(xiàn)代電子機(jī)載系統(tǒng)正由電子機(jī)械密集型向軟件密集型轉(zhuǎn)變,系統(tǒng)功能的實(shí)現(xiàn)越來(lái)越依賴于軟件,導(dǎo)致軟件的安全性對(duì)系統(tǒng)的安全至關(guān)重要。軟件測(cè)試是開發(fā)過程中用來(lái)驗(yàn)證軟件功能正確性的方法。然而,軟件功能的正確性不能保證安全關(guān)鍵系統(tǒng)的安全運(yùn)行。軟件必須根據(jù)安全分析確定的安全需求進(jìn)行驗(yàn)證并且需要識(shí)別出預(yù)期以外的功能,以確保識(shí)別出的潛在危險(xiǎn)行為不會(huì)發(fā)生。軟件的復(fù)雜性使得用傳統(tǒng)的安全性分析方法定義適當(dāng)?shù)能浖踩孕枨笞兊美щy。系統(tǒng)理論過程分析（System Theoretic Process Analysis,STPA）是一種基于系統(tǒng)理論事故模型和過程（Systems Theoretic Accident Model and Processes,STAMP）的安全性分析方法,用于識(shí)別系統(tǒng)危害,包括與軟件相關(guān)的危害,但是該方法嚴(yán)重依賴分析人員經(jīng)驗(yàn)。此外,目前在實(shí)際工程中采用基于模型的軟件開發(fā)方式成為趨勢(shì)。為此,本文以模型為核心,提出一種基于形式化擴(kuò)展STPA方法和RTCA DO-331適航標(biāo)準(zhǔn)相結(jié)合的機(jī)載軟件模型驗(yàn)證方法。本文的主要研究工作及創(chuàng)新點(diǎn)如下:（1）本文首先采用安全關(guān)鍵應(yīng)用開發(fā)環(huán)境（Safety Cr... 

【文章來(lái)源】：中國(guó)民航大學(xué)天津市

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

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

【部分圖文】：

起落架控制器軟件模型功能測(cè)試結(jié)果

中國(guó)民航大學(xué)碩士學(xué)位論文65經(jīng)分析得到了可能導(dǎo)致UCA18發(fā)生的危險(xiǎn)路徑RUCA18.4，實(shí)現(xiàn)對(duì)危險(xiǎn)行為的原因進(jìn)行定位，可以減少人為分析的工作量。定位后只需分析已給出的導(dǎo)致違反SSR18.4的路徑，反例的仿真結(jié)果如圖4-10(c)所示，反例總共給出了15個(gè)周期的交互場(chǎng)景，在第13個(gè)周期時(shí)，Res4輸出為false，說明此時(shí)軟件中存在違反SSR18.4的危險(xiǎn)行為，此時(shí)關(guān)鍵變量取值為flighttake_off,handledown,extend_EVopen,stateanormaly,對(duì)比RUCA18.4可知extend_EV信號(hào)出現(xiàn)錯(cuò)誤，有可能導(dǎo)致當(dāng)飛機(jī)處于起飛狀態(tài)并且飛機(jī)未離開地面時(shí)，起落架異常解鎖，導(dǎo)致事故發(fā)生。該系統(tǒng)級(jí)事故發(fā)生是由于提供extend_EV信號(hào)導(dǎo)致的，而該信號(hào)是在一個(gè)交互場(chǎng)景中被異常提供，在進(jìn)行模擬仿真時(shí)很難被發(fā)現(xiàn)，通過本文提供的系統(tǒng)安全性分析方法獲取的安全性需求，結(jié)合模型檢驗(yàn)技術(shù)識(shí)別出了潛在的致因場(chǎng)景導(dǎo)致軟件危險(xiǎn)行為的發(fā)生。圖4-10形式化驗(yàn)證結(jié)果基于已經(jīng)識(shí)別出來(lái)的危險(xiǎn)行為，通過對(duì)設(shè)計(jì)模型進(jìn)行修改，消除軟件中的潛在危險(xiǎn)行為，并重新進(jìn)行形式化驗(yàn)證識(shí)別潛在危險(xiǎn)行為。SCADE工具中針對(duì)形式化驗(yàn)證結(jié)果自動(dòng)生成驗(yàn)證報(bào)告，報(bào)告中以“valid”和“falsifiable”分別表示驗(yàn)證通過和不通過。在主機(jī)上執(zhí)行了4s的時(shí)間之后，驗(yàn)證結(jié)果顯示“valid”，如圖4-10所示。表明軟件模型通過了形式化驗(yàn)證，軟件中不存在違反STPA分析結(jié)果的執(zhí)行路徑。因此可以通過形式化擴(kuò)展STPA方法結(jié)合模型檢驗(yàn)技術(shù)有效識(shí)別出軟件中的危險(xiǎn)行為，并一定程度上提升了

中國(guó)民航大學(xué)碩士學(xué)位論文71圖5-2模型測(cè)試結(jié)果圖5-3模型測(cè)試結(jié)果報(bào)告通過基于需求進(jìn)行模型測(cè)試并生成測(cè)試結(jié)果報(bào)告表明軟件完備實(shí)現(xiàn)了預(yù)期的功能且測(cè)試結(jié)果是正確的。但是需要進(jìn)一步驗(yàn)證軟件中是否存在預(yù)期功能以外的功能。需要對(duì)軟件模型進(jìn)行模型覆蓋分析，通過模型覆蓋分析檢測(cè)軟件是否執(zhí)行了預(yù)期以外的功能。首先在SCADE工具中設(shè)置為MTC模式，并在MTC中設(shè)置為MC/DC覆蓋準(zhǔn)則，執(zhí)行覆蓋分析，最終覆蓋分析結(jié)果如圖5-4所示，并生成模型覆蓋報(bào)告如圖5-5所示。模型覆蓋結(jié)果表明：最終需求實(shí)現(xiàn)了對(duì)軟件模型的完全覆蓋，即模型中不存在預(yù)期以外的功能。在此過程中本文已對(duì)根據(jù)覆蓋分析結(jié)果對(duì)軟件進(jìn)行修改，消除了軟件中非預(yù)期的分支路徑。同時(shí)對(duì)生成的代碼進(jìn)行覆蓋分析，完成對(duì)軟件代碼的覆蓋分析，如圖5-6所示。SR1.1SR1.2SR1.3SR1.4測(cè)試總結(jié)：通過

【參考文獻(xiàn)】：
期刊論文
[1]基于STPA-Bayes模型的機(jī)載平視顯示系統(tǒng)安全性分析與評(píng)價(jià)[J]. 趙長(zhǎng)嘯,李浩,董磊,王鵬.  系統(tǒng)工程與電子技術(shù). 2020(05)
[2]基于STPA的安全分析方法在下一代列車運(yùn)行控制系統(tǒng)中的應(yīng)用[J]. 孫超.  鐵路計(jì)算機(jī)應(yīng)用. 2019(11)
[3]基于SCADE聯(lián)鎖邏輯實(shí)現(xiàn)與仿真分析[J]. 趙璐,張娜敏.  現(xiàn)代城市軌道交通. 2019(06)
[4]同步數(shù)據(jù)流語(yǔ)言可信編譯器的研究進(jìn)展[J]. 楊萍,王生原.  計(jì)算機(jī)科學(xué). 2019(05)
[5]波音737-8事故簡(jiǎn)析[J]. 馮建文,孫黎,劉金龍.  航空動(dòng)力. 2019(02)
[6]基于SCADE的列控系統(tǒng)車載ATP軟件建模研究[J]. 王錫奎,田建兆,王若昆,張菊.  高速鐵路技術(shù). 2019(01)
[7]基于模型的核電站操作員支持系統(tǒng)開發(fā)與測(cè)試[J]. 侯東,黃俊,王文全,沈軼燁.  上海交通大學(xué)學(xué)報(bào). 2018(S1)
[8]核電廠數(shù)字化儀控系統(tǒng)算法軟件自動(dòng)化生成方法[J]. 黃俊,李曉龍,趙洋,吳延群.  上海交通大學(xué)學(xué)報(bào). 2018(S1)
[9]Safety analysis of wheel brake system based on STAMP/STPA and Monte Carlo simulation[J]. HU Jianbo,ZHENG Lei,XU Shukui.  Journal of Systems Engineering and Electronics. 2018(06)
[10]形式化方法概貌[J]. 王戟,詹乃軍,馮新宇,劉志明.  軟件學(xué)報(bào). 2019(01)

碩士論文
[1]基于模型的無(wú)人機(jī)飛控系統(tǒng)建模及安全性驗(yàn)證方法研究[D]. 張品飛.電子科技大學(xué) 2017
[2]固定翼飛機(jī)飛行動(dòng)力學(xué)及振動(dòng)特性仿真研究[D]. 寧雷.哈爾濱工程大學(xué) 2016
[3]某型固定翼無(wú)人機(jī)飛控系統(tǒng)的設(shè)計(jì)與仿真[D]. 孔德勝.北京理工大學(xué) 2015
[4]基于模型的安全關(guān)鍵軟件全覆蓋測(cè)試方法的研究與實(shí)現(xiàn)[D]. 馬金梭.上海交通大學(xué) 2011
[5]SCADE在無(wú)人機(jī)飛行控制軟件設(shè)計(jì)中的應(yīng)用[D]. 程黎.西安電子科技大學(xué) 2011
[6]基于SCADE的無(wú)人機(jī)飛行控制軟件設(shè)計(jì)[D]. 顏雯清.南京航空航天大學(xué) 2008



本文編號(hào)：3386179