基于MARTE的综合航电系统配置信息分析与验证方法研究

发布时间：2018-05-25 03:21

本文选题：综合航电系统 + ARINC653配置信息　；参考：《南京航空航天大学》2015年硕士论文

【摘要】：近年来综合模块化航电系统(IMA)已经成为航空应用领域中出现的一类重要系统结构和发展趋势;其中一类IMA架构标准就是ARINC653标准,定义了IMA平台中操作系统层和应用软件层之间的标准接口(APEX)。满足ARINC653标准的IMA系统称之为ARINC653系统。在IMA架构中,系统的配置信息(Configuration)包含了整个体系结构中所有层次的相关信息,用来对IMA系统的硬件接口、操作系统和应用程序进行详尽的参数配置。因此,系统配置信息决定了ARINC653系统能否正确可靠的运行,如何保证配置信息的正确性和完整性已经成为当前综合航电系统研究领域的一个重要问题。本文工作主要以嵌入式系统建模与分析规范(MARTE)结合形式化验证方法来对ARINC653系统的配置信息的正确性以及相关分区任务可调度性问题展开研究,具体研究内容如下所述:1)针对符合ARINC653标准的IMA系统,结合多个实时应用在IMA平台上以时间/空间多分区形式运行的系统特征,建立了从系统配置信息的核心元素(包括模块、分区、内存、进程、通信等)到MARTE模型元素的语义映射规则,设计了基于模型驱动架构的系统配置信息模型转换的方法。2)针对ARINC653系统配置正确性验证需求,给出了一种对模型转换构造得到的系统配置信息MARTE模型进行形式化验证的框架;根据核心配置信息的语义验证需求,设计相应的REAL定理;基于REAL定理,对生成的模型文件进行需求约束的形式化验证;通过模型验证方法找出配置信息中的错误,使得可以及时调整相应模块的配置,提高系统的安全性和可靠性。3)研究了在ARINC653系统中多任务实时调度可满足性的问题,首先,考虑ARINC653分区系统的运行特征,采用MARTE建模语言对ARINC653系统的分层调度策略进行建模,然后通过MAST工具自定义调度策略,设计了对包含分区任务集调度信息的MARTE模型进行可调度性判定的算法。4)基于Papyrus建模平台,设计并实现了一个用于ARINC653配置文件建模与验证的原型工具CC653(Configuration Checker for ARINC653)。通过对CC653工具进行了相关实例分析,说明了此方法可以验证IMA系统配置信息的正确性、分区任务可调度性。
[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

【相似文献】