本文關(guān)鍵詞：基于AADL的綜合航電系統(tǒng)資源配置安全性分析與驗證

  更多相關(guān)文章： 綜合航空電子系統(tǒng) 基于模型驅(qū)動 ARINC653標(biāo)準(zhǔn) AADL模型 可靠性分析 可調(diào)度性分析

【摘要】：資源配置是綜合航空電子系統(tǒng)(IMA)設(shè)計的重要環(huán)節(jié),而配置信息是航空電子系統(tǒng)中的重要內(nèi)容,它存儲了系統(tǒng)軟硬件的參數(shù)信息,若配置信息發(fā)生錯誤則會導(dǎo)致系統(tǒng)無法正常運行,甚者會引發(fā)大型事故,所以配置信息的安全性分析顯得尤為重要,尤其是對其進(jìn)行可靠性和可調(diào)度性驗證。隨著嵌入式系統(tǒng)的規(guī)模越來越復(fù)雜以及安全需求的不斷提升,基于模型驅(qū)動的開發(fā)方法成為主流,而AADL也是現(xiàn)如今嵌入式實時系統(tǒng)領(lǐng)域模型驅(qū)動的新標(biāo)準(zhǔn),能更好地支持嵌入式系統(tǒng)軟硬件相結(jié)合的模型的建立,還能夠?qū)ο到y(tǒng)的可靠性、實時性等非功能屬性進(jìn)行很好的描述,因而在航空電子系統(tǒng)領(lǐng)域得到了廣泛的應(yīng)用。針對IMA系統(tǒng)配置信息的安全性驗證以及該配置信息對應(yīng)的IMA系統(tǒng)安全性分析的問題,本文基于AADL語言,在模型驅(qū)動開發(fā)方法下完成的主要工作如下:(1)分析了AADL模型元素和ARINC653配置信息的語義相似性,給出配置信息主要的核心概念與AADL模型元素的轉(zhuǎn)換規(guī)則,基于這些轉(zhuǎn)換規(guī)則將配置信息轉(zhuǎn)換成AADL模型,并使用REAL設(shè)計了相應(yīng)的可靠性驗證定理。(2)分析了轉(zhuǎn)換后的AADL模型,采用時間自動機(jī)形式化模型檢驗方法,設(shè)計了線程模板和調(diào)度器模板,根據(jù)轉(zhuǎn)換法則將AADL調(diào)度模型轉(zhuǎn)換到時間自動機(jī)模型,依據(jù)配置信息中系統(tǒng)可調(diào)度性驗證需求,在工具UPPAAL中對轉(zhuǎn)換得到的時間自動機(jī)進(jìn)行模擬和驗證,等價地驗證原模型的可調(diào)度性。(3)利用Eclipse插件開發(fā)技術(shù),設(shè)計了配置信息轉(zhuǎn)換與驗證插件并將其集成到了AADL建模與分析工具OSATE中,該插件具備如下功能:輸入配置信息文件,轉(zhuǎn)換成AADL模型后,結(jié)合REAL定理和Ocarina工具驗證配置信息的可靠性;通過文件解析,轉(zhuǎn)換生成時間自動機(jī)模型文件和性質(zhì)驗證查詢文件,自動調(diào)用UPPAAL工具驗證模型的可調(diào)度性。并給出了具體實例驗證了工具的正確性。(4)在資源配置AADL模型的基礎(chǔ)上,利用工具OSATE對該資源配置所支持的應(yīng)用操作層和功能層進(jìn)行建模和分析,同時使用AltaRica語言建立失效模型,結(jié)合工具SimFia自動生成故障樹。
【關(guān)鍵詞】：綜合航空電子系統(tǒng) 基于模型驅(qū)動 ARINC653標(biāo)準(zhǔn) AADL模型 可靠性分析 可調(diào)度性分析
【學(xué)位授予單位】：南京航空航天大學(xué)
【學(xué)位級別】：碩士
【學(xué)位授予年份】：2016
【分類號】：V243;TP309
【目錄】：

• 摘要4-6
• ABSTRACT6-14
• 第一章 緒論14-18
• 1.1 研究的背景與意義14-15
• 1.2 國內(nèi)外研究現(xiàn)狀及存在的問題15-17
• 1.3 主要研究內(nèi)容與論文結(jié)構(gòu)17-18
• 第二章 相關(guān)基礎(chǔ)知識18-34
• 2.1 綜合模塊化航電系統(tǒng)體系結(jié)構(gòu)概述18-19
• 2.2 ARINC653軟件體系結(jié)構(gòu)19-20
• 2.3 AADL20-27
• 2.3.1 組件（Component）21
• 2.3.2 組件類型（Component Type）21-22
• 2.3.3 組件實現(xiàn)（Component Implementation）22-23
• 2.3.4 組件交互（Components Interactions）23-25
• 2.3.5 模式（Modes）25
• 2.3.6 流（Flows）25-26
• 2.3.7 屬性（Properties）26
• 2.3.8 AADL模型工具26-27
• 2.4 時間自動機(jī)27-29
• 2.4.1 時間自動機(jī)理論27-28
• 2.4.2 基于時間自動機(jī)的驗證28-29
• 2.5 UPPAAL29-31
• 2.6 Alta Rica31-32
• 2.7 基于模型驅(qū)動的安全性分析過程32-33
• 2.8 本章小結(jié)33-34
• 第三章 IMA系統(tǒng)配置信息的轉(zhuǎn)換與驗證34-48
• 3.1 IMA系統(tǒng)配置信息轉(zhuǎn)換為AADL模型34-43
• 3.1.1 轉(zhuǎn)換規(guī)則35-41
• 3.1.2 模型轉(zhuǎn)換實例41-43
• 3.2 配置信息可靠性驗證43-47
• 3.2.1 REAL語言43-45
• 3.2.2 時間約束45
• 3.2.3 空間約束45-46
• 3.2.4 健康監(jiān)控約束46-47
• 3.3 本章小結(jié)47-48
• 第四章 AADL調(diào)度模型的轉(zhuǎn)換與驗證48-59
• 4.1 引言48-49
• 4.2 AADL調(diào)度模型與時間自動機(jī)模型的映射關(guān)系49-52
• 4.2.1 調(diào)度模型的形式化語義49-50
• 4.2.2 線程狀態(tài)轉(zhuǎn)換機(jī)制50-51
• 4.2.3 調(diào)度模型到時間自動機(jī)的語義映射51-52
• 4.3 調(diào)度模型時間自動機(jī)設(shè)計52-56
• 4.3.1 線程模板52-53
• 4.3.2 調(diào)度器模板53-56
• 4.4 可調(diào)度性驗證語句56-57
• 4.5 調(diào)度模型到時間自動機(jī)模型的轉(zhuǎn)換實例57-58
• 4.6 本章小結(jié)58-59
• 第五章 IMA系統(tǒng)配置信息轉(zhuǎn)換與驗證工具的實現(xiàn)59-72
• 5.1 引言59
• 5.2 配置信息文件解析59-61
• 5.3 AADL模型生成及驗證61-63
• 5.4 UPPAAL模型文件生成63-64
• 5.5 插件開發(fā)技術(shù)64-67
• 5.6 實例分析67-71
• 5.6.1 配置信息可靠性驗證67-69
• 5.6.2 配置信息可調(diào)度性驗證69-71
• 5.7 本章小結(jié)71-72
• 第六章 IMA資源配置安全性分析與驗證72-77
• 6.1 應(yīng)用操作層模式枚舉72-74
• 6.2 功能層建模74-76
• 6.3 本章小結(jié)76-77
• 第七章 總結(jié)及未來展望77-78
• 7.1 工作總結(jié)77
• 7.2 未來展望77-78
• 參考文獻(xiàn)78-82
• 致謝82-83
• 在學(xué)期間的研究成果及發(fā)表的學(xué)術(shù)論文83

【相似文獻(xiàn)】

中國期刊全文數(shù)據(jù)庫 前10條

1 劉柏;唐龍利;;艦船安全性分析技術(shù)研究[J];電子產(chǎn)品可靠性與環(huán)境試驗;2006年05期

2 王喜奎;劉春雷;;可靠性工程師資格考試輔導(dǎo)教材之六——安全性[J];質(zhì)量與可靠性;2008年04期

3 趙子建;任璐璐;;關(guān)于飛機(jī)區(qū)域安全性分析評價模型的構(gòu)建[J];科協(xié)論壇(下半月);2012年04期

4 馮福來;飛機(jī)區(qū)域安全性分析[J];航空標(biāo)準(zhǔn)化與質(zhì)量;1994年03期

5 單晨;孫景峰;;一卡通主要卡片的安全性分析[J];智能建筑;2009年10期

6 劉曉;蔣睿;;移動云計算中彈性存儲外包方案的安全性分析和改進(jìn)(英文)[J];Journal of Southeast University(English Edition);2012年04期

7 李曉磊;田瑾;趙廷弟;;改進(jìn)的區(qū)域安全性分析方法[J];航空學(xué)報;2008年03期

8 楊建蓉,孟立,王躍鴻;地區(qū)電網(wǎng)調(diào)度自動化系統(tǒng)安全性初探[J];山西電力;2005年03期

9 云平;姜紅旗;梁海燕;;大坡度滑索安全性分析[J];起重運輸機(jī)械;2011年08期

10 熊峻江,劉寶成,高宏;系統(tǒng)安全性分析與設(shè)計方法研究[J];北京航空航天大學(xué)學(xué)報;2002年02期

中國重要會議論文全文數(shù)據(jù)庫 前10條

1 文曉陽;高能;荊繼武;;論壇驗證碼技術(shù)的安全性分析[A];全國計算機(jī)安全學(xué)術(shù)交流會論文集（第二十二卷）[C];2007年

2 王丹琛;何大可;;密寫系統(tǒng)的安全性研究[A];2006中國西部青年通信學(xué)術(shù)會議論文集[C];2006年

3 范濤;鮑先巡;吳傳華;常勁松;彭代銀;;桑資源飲品的研究——靈芝桑茶的理化品質(zhì)與安全性分析[A];中國蠶學(xué)會第七次全國代表大會論文集[C];2003年

4 張兆心;方濱興;胡銘曾;張宏莉;;基于SIP網(wǎng)絡(luò)的安全性研究[A];全國網(wǎng)絡(luò)與信息安全技術(shù)研討會'2005論文集（上冊）[C];2005年

5 查月;高磊;;TCP/IP協(xié)議的安全性分析與防御[A];2008-2009年船舶通信導(dǎo)航論文集[C];2009年

6 林曦;高文建;何朝陽;薛峰;許劍冰;徐泰山;薛禹勝;汪磊;;廣西電網(wǎng)在線動態(tài)安全性分析系統(tǒng)[A];第三屆廣西青年學(xué)術(shù)年會論文集（自然科學(xué)篇）[C];2004年

7 林曦;高文建;何朝陽;薛峰;許劍冰;徐泰山;薛禹勝;汪磊;;廣西電網(wǎng)在線動態(tài)安全性分析系統(tǒng)[A];廣西電機(jī)工程學(xué)會第八屆青年學(xué)術(shù)年會論文集[C];2004年

8 海培華;;淺談GSM手機(jī)的安全性[A];中國通信學(xué)會第五屆學(xué)術(shù)年會論文集[C];2008年

9 馬瑞萍;;SSL安全性分析研究[A];第十六次全國計算機(jī)安全學(xué)術(shù)交流會論文集[C];2001年

10 陳偉杰;林宏基;;SOAP的安全性分析與整合[A];全國第16屆計算機(jī)科學(xué)與技術(shù)應(yīng)用（CACIS）學(xué)術(shù)會議論文集[C];2004年

中國重要報紙全文數(shù)據(jù)庫 前3條

1 ;如何提高SQL Server的安全性？[N];網(wǎng)絡(luò)世界;2008年

2 中國科學(xué)院動物研究所研究員 沈孝宙;關(guān)于GMO的對話[N];中國國門時報(中國出入境檢驗疫報);2001年

3 北京 Analysist;ExGB GuestBook安全性分析[N];電腦報;2001年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 張源;安卓平臺安全性增強關(guān)鍵技術(shù)的研究[D];復(fù)旦大學(xué);2014年

2 周淳;有限長誘騙態(tài)量子密鑰分配安全性研究[D];解放軍信息工程大學(xué);2014年

3 宋輝;隱密安全性機(jī)理研究[D];大連理工大學(xué);2011年

4 趙義博;量子密鑰分配的安全性研究[D];中國科學(xué)技術(shù)大學(xué);2009年

5 柴震川;門限密碼方案安全性和應(yīng)用研究[D];上海交通大學(xué);2007年

6 汪朝暉;橢圓曲線密碼的安全性研究[D];武漢大學(xué);2004年

7 范偉;移動商務(wù)安全性研究[D];北京郵電大學(xué);2010年

8 孫艷賓;公平交換協(xié)議的設(shè)計與安全性研究[D];北京郵電大學(xué);2011年

9 余斌霄;無線網(wǎng)絡(luò)的安全性[D];西安電子科技大學(xué);2006年

10 孔鴻濱;語義Web技術(shù)的本體安全性研究[D];云南大學(xué);2012年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 王晶;SSL/TLS的側(cè)信道攻擊[D];山東大學(xué);2015年

2 溫軒;實際QKD系統(tǒng)的安全性分析[D];哈爾濱工業(yè)大學(xué);2015年

3 牛磊;云存儲中數(shù)據(jù)審計協(xié)議的分析與設(shè)計[D];電子科技大學(xué);2014年

4 李文宇;城市道路無標(biāo)記路段穿越安全性研究[D];北京交通大學(xué);2016年

5 邢逆舟;基于模型的綜合化航電系統(tǒng)資源配置安全性分析與研究[D];南京航空航天大學(xué);2015年

6 孫健;基于AADL的綜合航電系統(tǒng)資源配置安全性分析與驗證[D];南京航空航天大學(xué);2016年

7 陳龍;IMA重配置策略和重配置的安全性分析方法研究[D];南京航空航天大學(xué);2016年

8 張貴;面向適航認(rèn)證的綜合化航電系統(tǒng)架構(gòu)安全性評估方法研究[D];南京航空航天大學(xué);2016年

9 李軍;艦船典型系統(tǒng)安全性分析評估方法研究[D];哈爾濱工程大學(xué);2012年

10 張旭光;火箭滑橇設(shè)計結(jié)構(gòu)安全性分析[D];南京理工大學(xué);2012年

，

本文編號：857588