【作者】 孙健；

【导师】 徐敏；

【作者基本信息】 南京航空航天大学 ， 软件工程， 2016， 硕士

【摘要】 资源配置是综合航空电子系统(IMA)设计的重要环节,而配置信息是航空电子系统中的重要内容,它存储了系统软硬件的参数信息,若配置信息发生错误则会导致系统无法正常运行,甚者会引发大型事故,所以配置信息的安全性分析显得尤为重要,尤其是对其进行可靠性和可调度性验证。随着嵌入式系统的规模越来越复杂以及安全需求的不断提升,基于模型驱动的开发方法成为主流,而AADL也是现如今嵌入式实时系统领域模型驱动的新标准,能更好地支持嵌入式系统软硬件相结合的模型的建立,还能够对系统的可靠性、实时性等非功能属性进行很好的描述,因而在航空电子系统领域得到了广泛的应用。针对IMA系统配置信息的安全性验证以及该配置信息对应的IMA系统安全性分析的问题,本文基于AADL语言,在模型驱动开发方法下完成的主要工作如下:(1)分析了AADL模型元素和ARINC653配置信息的语义相似性,给出配置信息主要的核心概念与AADL模型元素的转换规则,基于这些转换规则将配置信息转换成AADL模型,并使用REAL设计了相应的可靠性验证定理。(2)分析了转换后的AADL模型,采用时间自动机形式化模型检验方法,设计了线程模板和调度器模板,根据转换法则将AADL调度模型转换到时间自动机模型,依据配置信息中系统可调度性验证需求,在工具UPPAAL中对转换得到的时间自动机进行模拟和验证,等价地验证原模型的可调度性。(3)利用Eclipse插件开发技术,设计了配置信息转换与验证插件并将其集成到了AADL建模与分析工具OSATE中,该插件具备如下功能:输入配置信息文件,转换成AADL模型后,结合REAL定理和Ocarina工具验证配置信息的可靠性;通过文件解析,转换生成时间自动机模型文件和性质验证查询文件,自动调用UPPAAL工具验证模型的可调度性。并给出了具体实例验证了工具的正确性。(4)在资源配置AADL模型的基础上,利用工具OSATE对该资源配置所支持的应用操作层和功能层进行建模和分析,同时使用AltaRica语言建立失效模型,结合工具SimFia自动生成故障树。更多还原

【Abstract】 Resource allocation is a significant part of integrated modular avionics system(IMA) design, the system configuration information is also an important content of avionics system, which stores the parameters of the system software and hardware. The wrong configuration information can lead to abnormal operation of system and even lead to a large accident, so it is important to analyse the security of the configuration information, especially the verification of reliability and schedulability. With the increasing complexity of embedded systems and the continuous improvement of security requirements, model driven engineering(MDE), which is based on model, has become the mainstream. And AADL is a new standard for embedded real-time system, it can better support the establishment of the model of embedded system software and hardware, and also can describe the non functional properties of the system reliability, real-time, and so on. So it has been widely used in the field of aviation electronic systems.In view of reliability and schedulability verification of IMA system configuration information and the security analysis of the IMA system, the main work of this paper is as follows:(1) The semantics similarity of the AADL model elements and ARINC653 configuration information are respectively analyzed. The transformation rules of the key concepts of the configuration information and the AADL model elements are provided. Then use the rules to convert the configuration information into AADL model, and use REAL to design the corresponding relibability verification theorem.(2) The AADL model is analyzed, using the time automata formal analysis method to design thread timed automata templates and scheduler timed automata templates. And the mapping semantic between AADL scheduling model and timed automaton model is given to convert the AADL model into a time automaton model. According to the requirement of scheduling verification of the configuration information, the timed automate model is simulated and verified in the tool UPPAAL to analyse whether the original AADL model meets schedulability qualities.(3) Using Eclipse plug-in development technology to design configuration conversion and verification tool, and integrate it into the AADL modeling and analysis tool OSATE, the tool has following functions: Input configuration information file and convert it into AADL model, then combine with the REAL theorem and Ocarina tool to verify the reliability of the configuration information; through file parsing, convert and generate time automaton model file and property verification query file, and automatically open the UPPAAL tool to verify the schedulability of the model. And at last, an example is also given to verify the correctness of the tool.(4) On the basis of configuration information AADL model, the model of application layer and function layer are established in OSATE tool, and the failure model is established based on AltaRica language and the fault tree is researched using SimFia tool.更多还原