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

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

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

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

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