论文部分内容阅读
综合航电体系结构(IMA)的系统配置信息是航空电子系统中的核心内容，它保存着系统软件和硬件的参数信息，以及系统启动后所有构件的初始化信息。错误的配置信息轻者会导致系统无法正常运行，重者会带来飞机失事的惨剧。同时，为了满足系统实时性的要求，也要确保系统任务正常的执行。因此，在系统配置信息使用前，对配置信息进行可靠性和可调度性验证是非常重要的。模型驱动工程(MDE)以模型为中心，通过模型的设计、建立、分析验证来实现对安全关键系统的可靠性和可调度性验证。体系架构设计和分析语言(AADL)是一种符合模型驱动思想的语言，能有效的为安全关键系统进行建模设计和分析，已经广泛的应用在航空电子系统领域。针对上述提出的配置信息中系统可靠性与可调度性验证问题，本文提出了模型驱动的配置信息分析与验证方法，主要研究内容如下：(1)研究了模型驱动中的横向模型转换内容，分析了ARINC653配置信息与AADL模型元素的语义相似性，详细给出了配置信息中七个主要核心概念（模块、分区、进程、分区内通信、分区间通信、健康监控）与AADL模型元素的转换规则。基于这些转换规则，构造了配置信息向AADL模型转换的方法。(2)研究了模型验证语言REAL和REAL定理设计编写规则，依据配置信息中系统可靠性验证需求，使用REAL设计了相应的可靠性验证定理，构造了使用现有的模型分析套件Ocarina对转换生成的AADL模型进行可靠性验证的方法。(3)研究了IMA系统分区任务的调度模型和Cheddar自定义调度策略的方法，依据配置信息中系统可调度性验证需求，使用Cheddar设计了相应的分区任务调度策略，构造了使用Cheddar工具采用仿真的方式对AADL模型进行可调度性验证的方法。(4)设计了配置信息分析与验证工具ARINC653Verification，工具具备对配置信息进行可靠性验证的功能，由模型转换和模型验证两个子模块组成：模型转换模块，通过输入ARINC653配置文件，输出AADL模型文件；模型转换子模块，通过输入AADL模型和验证配置信息可靠性的REAL定理，输出验证结果。(5)给出了配置信息分析与验证方法的实例应用说明，包括：实例配置信息的XML文件内容；转换生成的AADL模型文件内容；配置信息中系统可靠性验证结果；配置信息中系统任务的仿真甘特图以及任务的最坏响应时间，给出了可调度性验证结果。