一种基于AADL的IMA系统配置信息的正确性检测方法  

Correctness Verification for Integrated Modular Avionics System Configuration Based on AADL Model

作　　者：胡军[1,2] 马金晶[1] 袁翔[1] 刘雪[1] 

机构地区：[1]南京航空航天大学计算机科学与技术学院,南京210016 [2]南京大学计算机软件新技术国家重点实验室,南京210093

出　　处：《南京航空航天大学学报》2014年第6期920-930,共11页Journal of Nanjing University of Aeronautics & Astronautics

基　　金：国家重点基础研究发展计划("九七三"计划)(2014CB744904)资助项目;回国留学人员科研启动基金(2012)资助项目;611航空科研基金(2012)资助项目;南京航空航天大学青年科技创新基金(NS2014098)资助项目

摘　　要：综合模块化航空电子系统(Integrated modular avionics,IMA)中的系统配置信息的正确性是保证IMA系统可靠运行的重要保障。配置信息的重配置给系统的更新和移植提供了方便,同时也给重配置后的系统带来了不安全因素。本文针对满足ARINC653规范的IMA系统重配置信息的正确性检测方法,展开了基于架构分析和设计语言(AADL)模型转换与分析的研究。给出了一系列从ARINC653系统配置信息到AADL模型元素的映射规则,包括模块、分区、进程、健康监控、通信等核心概念,并设计了一个模型转换的方法,然后采用一个第三方的工具对所得到的AADL模型展开配置信息正确性的语义验证。最后本文还给出了一个实例分析。The configuration information correctness of the integrated modular avionics （IMA） system is an important guarantee of operational reliability.Reconfiguration of configuration information provides conveniences for system updating and transplantation,and brings unsafe factors to system.Concerning the detection method for the correctness of the IMA system which satisfies ARINC653 specification,the transformation and analysis of the architecture analysis and design language （AADL） model are researched.Elements mapping rules from ARINC653 system configuration information to the AADL model are proposed,including module,partition,process,health,monitoring,communication and other core concepts.A model transformation approach is given,and a formal semantic verification of the configuration information correctness of AADL model is presented based on a third-party tool.Finally,an example analysis is provided.

关 键 词：软件可靠性测试 综合模块化航电系统 ARINC653配置信息 AADL REAL OSATE 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]