综合模块化航空电子系统重构与验证方法研究

发布时间：2020-06-18 19:06

【摘要】：为了满足飞机日益增长的军事和民用需求,综合模块化航空电子系统(Integrated Modular Avionics,IMA)近年来受到了工业界和学术界的广泛关注。IMA系统是安全攸关的嵌入式系统,当运行环境变化或组件故障时,系统对软件和硬件资源进行重构配置,保证功能和性能要求。重构必须严格遵照预先设定的策略执行,避免出现失控情况,引发系统故障。因此,重构设计过程中,如何对IMA系统资源进行分配,确保满足系统的功能性需求和安全性等质量属性要求,是整个飞机功能正常运行的关键。目前在IMA系统重构设计方面已取得了诸多研究进展和重要成果,但现有方法还面临以下挑战:首先,系统重构是逻辑架构到物理实现的重新映射,过程具有多样性和不确定性,且缺少对系统资源的精确描述,收集系统软件和硬件资源信息困难,重构自动化程度不高。其次,现有的验证方法在系统逻辑模型、物理架构模型、分区映射方面各有侧重,但缺少必要衔接,模型之间未建立统一的映射关系,验证结果的完整性有待提高。因此,通过基于模型的重构方法,简化映射过程,验证系统的功能性和安全性需求,实现对系统资源的重构配置,具有一定的研究意义和实用价值。本文围绕基于模型的IMA系统重构设计过程中建模、映射、验证、蓝图生成等内容进行详细讨论。论文的主要研究成果如下:(1)为保证重构后系统逻辑架构满足功能性需求,提出了一种SysML活动图的自动机模型构建和验证方法。采用扩展的有限自动机模型建模活动图内容和嵌套调用,使用线性时序逻辑表示功能性需求属性,通过相应的转换算法和模型检测方法确认设计的功能逻辑流程与需求的一致性。提出了一种基于模型的测试用例生成方法,将确认正确的活动图转为带约束的接口自动机,生成测试模型,通过其特有的乐观方法和博弈思想组合活动间的调用关系。然后在满足流约束条件组合覆盖准则的前提下,设计了测试用例生成算法,自动生成测试用例,用于架构的功能性测试。(2)为保证重构后系统逻辑架构满足安全性需求,提出了一种基于模型的系统安全性需求描述和验证方法。该方法针对系统功能需求、安全性目标和失效状态,建立危害用例,提取安全性需求;采用带功能失效的状态机图描述包含安全性需求的系统功能模型,并使用安全扩展层次自动机作为中间状态,通过转换算法实现系统功能模型的形式化描述,通过模型检测方法完成安全性需求验证。(3)为保证重构后系统物理架构满足安全性需求,提出了一种基于模型的组件错误行为描述和验证方法。该方法通过分析系统需求和安全性目标,建立物理架构模型,采用错误模型附件描述组件的错误行为和导致的故障影响;使用层次自动机作为中间状态,通过转换算法实现物理架构错误行为模型的形式化描述,采用模型检测验证故障影响是否满足安全性需求。(4)针对系统重配置、重映射过程复杂,功能性和安全性需求验证困难的问题,提出一种基于模式的IMA系统重构方法。将系统逻辑架构划分为多个层级,给出逻辑架构模型到AADL组件,以及AADL组件到ARINC653元素的映射规则;采用模式表示系统运行时资源配置,通过模式迁移实现不同层级的重构设计,并对各模式下的系统逻辑架构和映射所得的物理架构模型进行验证和分析;构建系统蓝图生成算法,根据模式迁移和验证结果自动生成重构蓝图,指导系统资源动态配置,实现相应的功能。
【学位授予单位】：西北大学
【学位级别】：博士
【学位授予年份】：2019
【分类号】：V243;TP311.52
【图文】：

性质(3.1)的验证结果

性质(3.1)的反例路径

【参考文献】

相关硕士学位论文 前2条

1 张潇;基于模型驱动的IMA资源安全分配与验证方法研究[D];南京航空航天大学;2016年

2 邢逆舟;基于模型的综合化航电系统资源配置安全性分析与研究[D];南京航空航天大学;2015年

本文编号：2719700