基于MARTE的綜合航電系統(tǒng)配置信息分析與驗證方法研究.pdf

1、近年來綜合模塊化航電系統(tǒng)(IMA)已經(jīng)成為航空應(yīng)用領(lǐng)域中出現(xiàn)的一類重要系統(tǒng)結(jié)構(gòu)和發(fā)展趨勢；其中一類IMA架構(gòu)標(biāo)準(zhǔn)就是ARINC653標(biāo)準(zhǔn)，定義了IMA平臺中操作系統(tǒng)層和應(yīng)用軟件層之間的標(biāo)準(zhǔn)接口(APEX)。滿足ARINC653標(biāo)準(zhǔn)的IMA系統(tǒng)稱之為ARINC653系統(tǒng)。在IMA架構(gòu)中，系統(tǒng)的配置信息(Configuration)包含了整個體系結(jié)構(gòu)中所有層次的相關(guān)信息,用來對IMA系統(tǒng)的硬件接口、操作系統(tǒng)和應(yīng)用程序進(jìn)行詳盡的參數(shù)配置。因此

2、，系統(tǒng)配置信息決定了ARINC653系統(tǒng)能否正確可靠的運行，如何保證配置信息的正確性和完整性已經(jīng)成為當(dāng)前綜合航電系統(tǒng)研究領(lǐng)域的一個重要問題。
　　本文工作主要以嵌入式系統(tǒng)建模與分析規(guī)范(MARTE)結(jié)合形式化驗證方法來對ARINC653系統(tǒng)的配置信息的正確性以及相關(guān)分區(qū)任務(wù)可調(diào)度性問題展開研究，具體研究內(nèi)容如下所述：
　　1)針對符合ARINC653標(biāo)準(zhǔn)的IMA系統(tǒng)，結(jié)合多個實時應(yīng)用在IMA平臺上以時間/空間多分區(qū)形式運行的

3、系統(tǒng)特征，建立了從系統(tǒng)配置信息的核心元素(包括模塊、分區(qū)、內(nèi)存、進(jìn)程、通信等)到MARTE模型元素的語義映射規(guī)則，設(shè)計了基于模型驅(qū)動架構(gòu)的系統(tǒng)配置信息模型轉(zhuǎn)換的方法。
　　2)針對ARINC653系統(tǒng)配置正確性驗證需求，給出了一種對模型轉(zhuǎn)換構(gòu)造得到的系統(tǒng)配置信息MARTE模型進(jìn)行形式化驗證的框架；根據(jù)核心配置信息的語義驗證需求，設(shè)計相應(yīng)的REAL定理；基于REAL定理，對生成的模型文件進(jìn)行需求約束的形式化驗證；通過模型驗證方法找出

4、配置信息中的錯誤，使得可以及時調(diào)整相應(yīng)模塊的配置，提高系統(tǒng)的安全性和可靠性。
　　3)研究了在ARINC653系統(tǒng)中多任務(wù)實時調(diào)度可滿足性的問題，首先，考慮ARINC653分區(qū)系統(tǒng)的運行特征，采用MARTE建模語言對ARINC653系統(tǒng)的分層調(diào)度策略進(jìn)行建模，然后通過MAST工具自定義調(diào)度策略，設(shè)計了對包含分區(qū)任務(wù)集調(diào)度信息的MARTE模型進(jìn)行可調(diào)度性判定的算法。
　　4)基于Papyrus建模平臺，設(shè)計并實現(xiàn)了一個用于AR