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

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

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

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

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