模型驅(qū)動的綜合航電系統(tǒng)配置信息的分析與驗證方法研究.pdf

1、綜合航電體系結(jié)構(gòu)(IMA)的系統(tǒng)配置信息是航空電子系統(tǒng)中的核心內(nèi)容,它保存著系統(tǒng)軟件和硬件的參數(shù)信息,以及系統(tǒng)啟動后所有構(gòu)件的初始化信息。錯誤的配置信息輕者會導(dǎo)致系統(tǒng)無法正常運行,重者會帶來飛機(jī)失事的慘劇。同時,為了滿足系統(tǒng)實時性的要求,也要確保系統(tǒng)任務(wù)正常的執(zhí)行。因此,在系統(tǒng)配置信息使用前,對配置信息進(jìn)行可靠性和可調(diào)度性驗證是非常重要的。模型驅(qū)動工程(MDE)以模型為中心,通過模型的設(shè)計、建立、分析驗證來實現(xiàn)對安全關(guān)鍵系統(tǒng)的可靠性和可

2、調(diào)度性驗證。體系架構(gòu)設(shè)計和分析語言(AADL)是一種符合模型驅(qū)動思想的語言,能有效的為安全關(guān)鍵系統(tǒng)進(jìn)行建模設(shè)計和分析,已經(jīng)廣泛的應(yīng)用在航空電子系統(tǒng)領(lǐng)域。
　　針對上述提出的配置信息中系統(tǒng)可靠性與可調(diào)度性驗證問題,本文提出了模型驅(qū)動的配置信息分析與驗證方法,主要研究內(nèi)容如下:
　　(1)研究了模型驅(qū)動中的橫向模型轉(zhuǎn)換內(nèi)容,分析了ARINC653配置信息與AADL模型元素的語義相似性,詳細(xì)給出了配置信息中七個主要核心概念(模塊、

3、分區(qū)、進(jìn)程、分區(qū)內(nèi)通信、分區(qū)間通信、健康監(jiān)控)與AADL模型元素的轉(zhuǎn)換規(guī)則?；谶@些轉(zhuǎn)換規(guī)則,構(gòu)造了配置信息向AADL模型轉(zhuǎn)換的方法。
　　(2)研究了模型驗證語言REAL和REAL定理設(shè)計編寫規(guī)則,依據(jù)配置信息中系統(tǒng)可靠性驗證需求,使用REAL設(shè)計了相應(yīng)的可靠性驗證定理,構(gòu)造了使用現(xiàn)有的模型分析套件Ocarin a對轉(zhuǎn)換生成的AADL模型進(jìn)行可靠性驗證的方法。
　　(3)研究了IMA系統(tǒng)分區(qū)任務(wù)的調(diào)度模型和Cheddar自

4、定義調(diào)度策略的方法,依據(jù)配置信息中系統(tǒng)可調(diào)度性驗證需求,使用Cheddar設(shè)計了相應(yīng)的分區(qū)任務(wù)調(diào)度策略,構(gòu)造了使用Ched dar工具采用仿真的方式對AADL模型進(jìn)行可調(diào)度性驗證的方法。
　　(4)設(shè)計了配置信息分析與驗證工具ARINC653Verification,工具具備對配置信息進(jìn)行可靠性驗證的功能,由模型轉(zhuǎn)換和模型驗證兩個子模塊組成:模型轉(zhuǎn)換模塊,通過輸入 ARINC653配置文件,輸出 AADL模型文件;模型轉(zhuǎn)換子模塊,