论文部分内容阅读
近年来综合模块化航电系统(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系统配置信息的正确性、分区任务可调度性。