● 摘要
为了满足航电系统软件对高可靠性等要求，在1997年美国航空电子工程协会（AEEC）发布了航电系统应用软件标准接口（ARINC653标准）。目前，ARINC653已经发展为是航电的主要的行业标准，它定义了用于航电系统设计的一系列功能。但是ARINC653只是给出相关的标准，并没有给出表示相关概念的抽象符号。因此，2011年，SAE发布了基于AADL的ARINC653附件用于描述ARINC653标准，并且作为模型驱动（Model Driven Architecture，MDA）领域的佼佼者AADL不仅能描述嵌入式的软硬件结构，而且能验证嵌入式软件中相关的非功能性属性。
但是在实际应用中，ARINC653附件仅仅是通过自然语言描述了相关的映射关系，这对于开发人员来说，容易造成误解，产生二义性，并且AADL中存在没有明确定义一种机制来执行相关领域约束检查的缺陷，容易导致开发人员在建模时违反了ARINC653标准中潜在的领域约束。虽然ARINC653标准中规定两层调度的机制，但在并没有给出相应的分区设计标准，其给出基于时间片轮转的调度算法，虽然简单，但往往产生空闲分区，导致资源的浪费。与之同时，软件的复杂性也带来了软件可靠性的问题，但基于AADL的ARINC653错误模型只能表示为一个静态的系统模型，这对于分析可靠性模型中组件之间的交互的动态行为带来不便。因此，本文针对于上述问题，做了以下方面的研究：
首先，本文把ARINC653软件划分为分区模型、分区内任务模型和错误模型，利用数学定义形式描述了模型中ARINC653标准所定义的相关元素与AADL标准中所定义的元素之间的关系，并利用约束分析语言（REAL，Requirements Enforce- ment Analysis Language）对模型执行ARINC653领域约束检查，从而避免模型与领域约束不一致的情况。
其次给出基于加权轮转的ARINC653调度策略。定义分区权重计算公式，分区以权重方式轮转运行，分区内调度以RMS作为调度算法。并对AADL开源集成开发环境（OSATE）进行二次开发以便支持两层调度，从而对该调度策略进行调度分析。
最后，基于AADL的ARINC653错误模型只能表示为一个静态的系统模型的缺陷，为了更好评估基于AADL的ARINC653模型的可靠性，从错误的基本概念、错误的传播、错误的过滤/屏蔽方面考虑，提出相关的转换规则，把基于AADL的ARINC653模型转换为广义随机Petri网。并依托随机petri网分析技术进行可靠性评估。