基于AADL的綜合航電系統(tǒng)資源配置安全性分析與驗(yàn)證.pdf

1、資源配置是綜合航空電子系統(tǒng)(IMA)設(shè)計(jì)的重要環(huán)節(jié)，而配置信息是航空電子系統(tǒng)中的重要內(nèi)容，它存儲了系統(tǒng)軟硬件的參數(shù)信息，若配置信息發(fā)生錯誤則會導(dǎo)致系統(tǒng)無法正常運(yùn)行，甚者會引發(fā)大型事故，所以配置信息的安全性分析顯得尤為重要，尤其是對其進(jìn)行可靠性和可調(diào)度性驗(yàn)證。隨著嵌入式系統(tǒng)的規(guī)模越來越復(fù)雜以及安全需求的不斷提升，基于模型驅(qū)動的開發(fā)方法成為主流，而AADL也是現(xiàn)如今嵌入式實(shí)時系統(tǒng)領(lǐng)域模型驅(qū)動的新標(biāo)準(zhǔn)，能更好地支持嵌入式系統(tǒng)軟硬件相結(jié)合的模型

2、的建立，還能夠?qū)ο到y(tǒng)的可靠性、實(shí)時性等非功能屬性進(jìn)行很好的描述，因而在航空電子系統(tǒng)領(lǐng)域得到了廣泛的應(yīng)用。
　　針對IMA系統(tǒng)配置信息的安全性驗(yàn)證以及該配置信息對應(yīng)的IMA系統(tǒng)安全性分析的問題，本文基于AADL語言，在模型驅(qū)動開發(fā)方法下完成的主要工作如下：
　?。?）分析了AADL模型元素和ARINC653配置信息的語義相似性，給出配置信息主要的核心概念與AADL模型元素的轉(zhuǎn)換規(guī)則，基于這些轉(zhuǎn)換規(guī)則將配置信息轉(zhuǎn)換成AADL模型

3、，并使用REAL設(shè)計(jì)了相應(yīng)的可靠性驗(yàn)證定理。
　?。?）分析了轉(zhuǎn)換后的AADL模型，采用時間自動機(jī)形式化模型檢驗(yàn)方法，設(shè)計(jì)了線程模板和調(diào)度器模板，根據(jù)轉(zhuǎn)換法則將AADL調(diào)度模型轉(zhuǎn)換到時間自動機(jī)模型，依據(jù)配置信息中系統(tǒng)可調(diào)度性驗(yàn)證需求，在工具UPPAAL中對轉(zhuǎn)換得到的時間自動機(jī)進(jìn)行模擬和驗(yàn)證，等價(jià)地驗(yàn)證原模型的可調(diào)度性。
　?。?）利用Eclipse插件開發(fā)技術(shù)，設(shè)計(jì)了配置信息轉(zhuǎn)換與驗(yàn)證插件并將其集成到了AADL建模與分析工具

4、OSATE中，該插件具備如下功能：輸入配置信息文件，轉(zhuǎn)換成AADL模型后，結(jié)合REAL定理和Ocarina工具驗(yàn)證配置信息的可靠性；通過文件解析，轉(zhuǎn)換生成時間自動機(jī)模型文件和性質(zhì)驗(yàn)證查詢文件，自動調(diào)用UPPAAL工具驗(yàn)證模型的可調(diào)度性。并給出了具體實(shí)例驗(yàn)證了工具的正確性。
　　（4）在資源配置AADL模型的基礎(chǔ)上，利用工具OSATE對該資源配置所支持的應(yīng)用操作層和功能層進(jìn)行建模和分析，同時使用AltaRica語言建立失效模型，結(jié)合