本文選題：綜合航電系統(tǒng) + ARINC653配置信息��； 參考：《南京航空航天大學》2015年碩士論文

【摘要】：近年來綜合模塊化航電系統(tǒng)(IMA)已經(jīng)成為航空應(yīng)用領(lǐng)域中出現(xiàn)的一類重要系統(tǒng)結(jié)構(gòu)和發(fā)展趨勢;其中一類IMA架構(gòu)標準就是ARINC653標準,定義了IMA平臺中操作系統(tǒng)層和應(yīng)用軟件層之間的標準接口(APEX)。滿足ARINC653標準的IMA系統(tǒng)稱之為ARINC653系統(tǒng)。在IMA架構(gòu)中,系統(tǒng)的配置信息(Configuration)包含了整個體系結(jié)構(gòu)中所有層次的相關(guān)信息,用來對IMA系統(tǒng)的硬件接口、操作系統(tǒng)和應(yīng)用程序進行詳盡的參數(shù)配置。因此,系統(tǒng)配置信息決定了ARINC653系統(tǒng)能否正確可靠的運行,如何保證配置信息的正確性和完整性已經(jīng)成為當前綜合航電系統(tǒng)研究領(lǐng)域的一個重要問題。本文工作主要以嵌入式系統(tǒng)建模與分析規(guī)范(MARTE)結(jié)合形式化驗證方法來對ARINC653系統(tǒng)的配置信息的正確性以及相關(guān)分區(qū)任務(wù)可調(diào)度性問題展開研究,具體研究內(nèi)容如下所述:1)針對符合ARINC653標準的IMA系統(tǒng),結(jié)合多個實時應(yīng)用在IMA平臺上以時間/空間多分區(qū)形式運行的系統(tǒng)特征,建立了從系統(tǒng)配置信息的核心元素(包括模塊、分區(qū)、內(nèi)存、進程、通信等)到MARTE模型元素的語義映射規(guī)則,設(shè)計了基于模型驅(qū)動架構(gòu)的系統(tǒng)配置信息模型轉(zhuǎn)換的方法。2)針對ARINC653系統(tǒng)配置正確性驗證需求,給出了一種對模型轉(zhuǎn)換構(gòu)造得到的系統(tǒng)配置信息MARTE模型進行形式化驗證的框架;根據(jù)核心配置信息的語義驗證需求,設(shè)計相應(yīng)的REAL定理;基于REAL定理,對生成的模型文件進行需求約束的形式化驗證;通過模型驗證方法找出配置信息中的錯誤,使得可以及時調(diào)整相應(yīng)模塊的配置,提高系統(tǒng)的安全性和可靠性。3)研究了在ARINC653系統(tǒng)中多任務(wù)實時調(diào)度可滿足性的問題,首先,考慮ARINC653分區(qū)系統(tǒng)的運行特征,采用MARTE建模語言對ARINC653系統(tǒng)的分層調(diào)度策略進行建模,然后通過MAST工具自定義調(diào)度策略,設(shè)計了對包含分區(qū)任務(wù)集調(diào)度信息的MARTE模型進行可調(diào)度性判定的算法。4)基于Papyrus建模平臺,設(shè)計并實現(xiàn)了一個用于ARINC653配置文件建模與驗證的原型工具CC653(Configuration Checker for ARINC653)。通過對CC653工具進行了相關(guān)實例分析,說明了此方法可以驗證IMA系統(tǒng)配置信息的正確性、分區(qū)任務(wù)可調(diào)度性。
[Abstract]:In recent years, Integrated Modular Avionics system (IMA) has become a kind of important system structure and development trend in aviation application field, among which a kind of IMA architecture standard is ARINC653 standard. The standard interface between operating system layer and application software layer in IMA platform is defined. A IMA system that meets the ARINC653 standard is called a ARINC653 system. In the IMA architecture, the configuration information of the system includes all the relevant information in the whole architecture, which is used to configure the hardware interface, operating system and application program of the IMA system in detail. Therefore, the system configuration information determines whether the ARINC653 system can operate correctly and reliably. How to ensure the correctness and integrity of the configuration information has become an important issue in the field of integrated avionics system research. In this paper, the embedded system Modeling and Analysis Specification (MART) combined with formal verification method is used to study the correctness of configuration information of ARINC653 system and the schedulability of relevant partition tasks. The specific research contents are as follows: (1) in view of the IMA system that conforms to the ARINC653 standard, combined with the system characteristics of multiple real-time applications running on the IMA platform in the form of multiple time / space partitions, the core elements (including modules) of the configuration information of the slave system are established. The semantic mapping rules from partitioning, memory, process, communication) to MARTE model elements, and the method of model driven architecture based system configuration information model transformation. 2) is designed to verify the correctness of ARINC653 system configuration. This paper presents a formal verification framework for the system configuration information MARTE model constructed by model transformation, designs the corresponding REAL theorem according to the semantic verification requirements of the core configuration information, and designs the corresponding REAL theorem based on the REAL theorem. The model files are formalized to verify the requirements constraints, and the errors in the configuration information can be found by the model verification method, so that the configuration of the corresponding modules can be adjusted in time. Improving the security and reliability of the system. 3) the problem of multitask real-time scheduling satisfiability in ARINC653 system is studied. Firstly, considering the running characteristics of ARINC653 partitioning system, the hierarchical scheduling strategy of ARINC653 system is modeled by MARTE modeling language. Then, by using the MAST tool to define the scheduling strategy, the schedulability decision algorithm for the MARTE model containing the partition task set scheduling information is designed. 4) based on the Papyrus modeling platform. A prototype tool CC653(Configuration Checker for ARINC653 for modeling and verifying ARINC653 configuration files is designed and implemented. Through the analysis of CC653 tools, it is proved that this method can verify the correctness of configuration information of IMA system and the schedulability of partition tasks.
【學位授予單位】：南京航空航天大學
【學位級別】：碩士
【學位授予年份】：2015
【分類號】：V243

【相似文獻】

相關(guān)期刊論文 前1條

1 吳代輝;唐朔飛;季振洲;王凱峰;康海濤;;RFAI:基于硬件捕獲配置信息[J];哈爾濱工業(yè)大學學報;2006年10期

相關(guān)重要報紙文章 前2條

1 柳相鐵;用IPSwitcher修改網(wǎng)絡(luò)配置信息[N];電腦報;2004年

2 于翔;四大特性鑄就成熟的CMDB[N];網(wǎng)絡(luò)世界;2006年

相關(guān)碩士學位論文 前2條

1 馬金晶;基于MARTE的綜合航電系統(tǒng)配置信息分析與驗證方法研究[D];南京航空航天大學;2015年

2 袁翔;模型驅(qū)動的綜合航電系統(tǒng)配置信息的分析與驗證方法研究[D];南京航空航天大學;2014年

，

本文編號：1931855