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

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

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

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

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