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

摘要

近年来综合模块化航电系统(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(ConfigurationCheckerfor ARINC653)。通过对CC653工具进行了相关实例分析，说明了此方法可以验证IMA系统配置信息的正确性、分区任务可调度性。

目录

封面

声明

中文摘要

英文摘要

目录

缩略词

第一章 绪论

1.1 课题研究背景

1.2 国内外研究现状

1.3 本文研究内容与论文结构

第二章 面向综合航电系统配置信息的正确性分析框架

2.1 综合航电系统标准概述

2.2 实时嵌入式系统建模与分析建模语言概述

2.3 面向综合航电系统的配置信息的正确性分析框架

2.4 本章小结

第三章 基于MARTE的IMA系统配置信息建模与正确性验证

3.1 ARINC653系统配置信息核心概念建模

3.2 ARINC653系统配置信息转换规则

3.3 配置信息模型的分析与验证

3.4 本章小结

第四章 基于MARTE的IMA分区任务集可调度性判定方法

4.1 IMA分区调度特征

4.2 IMA分区调度判定分析

4.3 可调度性判定框架

4.4 本章小结

第五章 ARINC653系统配置信息验证工具设计与实现

5.1 ARINC653系统配置信息验证工具设计

5.2 ARINC653系统配置信息验证工具实现

5.3 IMA系统配置信息正确性和可调度性实例分析

5.4 本章小结

第六章 总结与展望

6.1 论文总结

6.2 未来工作展望

参考文献

致谢

在学期间的研究成果及发表的学术论文