论文部分内容阅读
资源配置是综合航空电子系统(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自动生成故障树。