模型驱动的综合航电系统配置信息的分析与验证方法研究.pdf

1、综合航电体系结构(IMA)的系统配置信息是航空电子系统中的核心内容,它保存着系统软件和硬件的参数信息,以及系统启动后所有构件的初始化信息。错误的配置信息轻者会导致系统无法正常运行,重者会带来飞机失事的惨剧。同时,为了满足系统实时性的要求,也要确保系统任务正常的执行。因此,在系统配置信息使用前,对配置信息进行可靠性和可调度性验证是非常重要的。模型驱动工程(MDE)以模型为中心,通过模型的设计、建立、分析验证来实现对安全关键系统的可靠性和可

2、调度性验证。体系架构设计和分析语言(AADL)是一种符合模型驱动思想的语言,能有效的为安全关键系统进行建模设计和分析,已经广泛的应用在航空电子系统领域。
　　针对上述提出的配置信息中系统可靠性与可调度性验证问题,本文提出了模型驱动的配置信息分析与验证方法,主要研究内容如下:
　　(1)研究了模型驱动中的横向模型转换内容,分析了ARINC653配置信息与AADL模型元素的语义相似性,详细给出了配置信息中七个主要核心概念(模块、

3、分区、进程、分区内通信、分区间通信、健康监控)与AADL模型元素的转换规则。基于这些转换规则,构造了配置信息向AADL模型转换的方法。
　　(2)研究了模型验证语言REAL和REAL定理设计编写规则,依据配置信息中系统可靠性验证需求,使用REAL设计了相应的可靠性验证定理,构造了使用现有的模型分析套件Ocarin a对转换生成的AADL模型进行可靠性验证的方法。
　　(3)研究了IMA系统分区任务的调度模型和Cheddar自

4、定义调度策略的方法,依据配置信息中系统可调度性验证需求,使用Cheddar设计了相应的分区任务调度策略,构造了使用Ched dar工具采用仿真的方式对AADL模型进行可调度性验证的方法。
　　(4)设计了配置信息分析与验证工具ARINC653Verification,工具具备对配置信息进行可靠性验证的功能,由模型转换和模型验证两个子模块组成:模型转换模块,通过输入 ARINC653配置文件,输出 AADL模型文件;模型转换子模块,