当前位置:问答库>论文摘要

题目:基于AADL的嵌入式软件系统验证技术研究

关键词:AADL;ARINC653;模型转换;可靠性;可调度性

  摘要


                                                  摘  要

       随着嵌入式系统的迅猛发展,其结构也越来越复杂,尤其在航空电子系统方面,已经发展为综合模块化系统。与此同时,对于系统的安全性、可靠性等非功能属性方面的要求也越来越高。为了满足此需求,美国航空电子工程协会在1997年发布了ARINC653标准,即航空电子系统应用软件接口标准,经过多年的发展,已经成为航空电子系统的主要行业标准。但是ARINC653只是给出了相关标准,并没有给出表示相关概念的抽象符号。因此,美国机动车工程师学会于2011基于AADL建模语言发布了ARINC653附件,通过此附件对ARINC653标准进行描述。在多个附件的协助下,AADL不仅可以描述嵌入式系统的软硬件结构,还能分析验证嵌入式系统中相关的非功能属性。

       虽然ARINC653标准中规定了双层调度机制,但并没有给出相应的分区设计标准,而且其中的基于主时间框架轮转调度算法,虽然简单易懂,但存在空闲时间浪费的缺陷。除此之外,软件的复杂性也带来了软件可靠性方面的问题。AADL虽然可通过错误模型对系统的可靠性问题进行描述,但其只能表示为静态系统模型,难以对系统可靠性模型中组件之间的动态交互行为进行分析。由于存在上述的种种问题,本论文就嵌入式系统非功能属性验证做了以下几个方面的研究:

       (1)首先,将基于优先级的分区调度机制应用于ARINC653软件中。因为基于优先级的分区调度机制允许多个分区以优先级的方式抢占主时间框架中的空闲时间,从而可以弥补ARINC653标准定义的调度机制空闲时间浪费的缺陷。其次,为了对本论文所采用的基于优先级的分区调度机制进行可调度性分析,本文对AADL开源集成开发环境(OSATE)进行了二次开发。

       (2)AADL错误模型存在只能静态描述系统的缺陷,为了更好的对可靠性模型进行分析,本文依据错误模型的基本概念、错误传播、错误过滤等多个方面,提出了相关转换规则,将基于AADL 的可靠性模型转换为故障树,并依据现有故障树分析方法对软件的可靠性进行验证。

       (3)应用AADL开源集成开发环境(OSATE)对飞行规划子系统实例进行了可调度性和可靠性分析验证。实验结果表明,本文采用的基于优先级的分区调度机制在一定程度上改善了ARINC653标准调度机制的空闲时间浪费,并且采用将可靠性模型转换为故障树的方法可以有效验证系统的可靠性。

 关键词:AADL,ARINC653,模型转换,可靠性,可调度性