基于体系结构模型的综合化航电分区可调度性验证

刘哲旭 樊智勇 赵 珍

1(中国民航大学电子信息与自动化学院 天津 300300)2(中国民航大学工程技术训练中心 天津 300300)

0 引 言

现代新型飞机电子设备已快速进入综合模块化航空电子系统(Integrated Modular Avionics，IMA)的崭新时代[1]。在民用航空领域，欧洲Airbus和美国Boeing均率先将先进的IMA航电架构应用于新一代民用客机(A380和B787)，而我国的国产大型客机C919也将航电系统的综合模块化技术作为飞机研制的关键。

IMA作为安全关键的复杂嵌入式系统，其软件系统的可靠性和安全性是保证飞行安全的必要条件[2-5]。为此，IMA软件接口开发规范ARINC653将“分区”作为系统软件开发的核心理念。这种方式可以隔离资源分配和应用，避免了应用间错误的相互影响，从而提高了系统的容错性。然而，由于IMA采用了分区层调度和任务层调度的双层调度机制，这使得系统中任务的调度和执行更加复杂，传统的可调度分析方法已不再适用[6-7]。

近年来，模型驱动的开发方法(Model driven development，MDD)在IMA等复杂嵌入式系统的设计和验证领域得到了广泛应用。由于其能够在开发阶段对系统进行分析与验证，有助于保证系统的质量属性，并可以有效地控制开发时间与成本。目前，针对IMA系统的分区调度问题，基于MDD的方法已取得了一些研究成果。文献[8]采用统一建模语言(Unified Modeling Language，UML)建立了IMA软件系统的分区调度过程模型，提出了分区配置和启动机制的设计策略。文献[9-10]采用实时嵌入式系统建模与分析语言(modeling and analysis of real time and embedded systems，MARTE)对IMA的分区调度问题进行研究，通过建立系统的MARTE模型对IMA分区的时间资源配置进行了验证。但是，由于上述方法在本质上都是多模型多分析的方法，其在分析系统不同属性时所建立的模型存在不一致性，这不利于复杂嵌入式系统的整体验证[11]。

体系结构分析与设计语言(Architecture Analysis & Design Language，AADL)是由美国汽车工程师协会于2004年提出的一种用于嵌入式实时系统设计和开发的MDD工具。与上述方法相比，AADL只需通过建立单一模型即可支持系统多种关键属性的分析，可以将系统的分析和验证融合于统一框架之下，因此，已逐渐成为IMA等复杂嵌入式系统关键属性验证的标准建模语言[12-15]。目前，针对复杂嵌入式系统AADL模型的可调度性验证方法均采用了模型转换的方式。文献[16-17]在建立系统AADL模型的基础上，讨论了AADL模型到时间自动机的转换，并使用UPPAAL工具实现了可调度验证。文献[18]将IMA分区资源配置的AADL模型转换为着色Petri网模型，通过着色Petri网描述了AADL模型中的时间资源和物理资源，并可在此基础上进行分区可调度性验证。然而，上述方法中的AADL模型均不能描述系统中任务调度的动态行为，因此不能直接用于系统的可调度性验证。验证时，还需要对AADL模型进行转换或二次建模，这一过程是比较繁琐的。

为解决上述问题，本文提出了基于AADL的IMA分区可调度性验证模型的建模方法，并在此基础上对其可调度性验证方法进行研究，避免了现有方法中繁琐的二次建模过程。

1 IMA分区调度原理

1.1 IMA分区架构

ARINC653标准中定义的IMA架构如图1所示，与一般嵌入式系统类似，由硬件和软件两部分组成。图1中，IMA模块的软件部分可以进一步划分为分区应用软件与核心软件(ARINC653操作系统)。其中，分区应用软件用于实现航空电子设备的各种特定功能，如飞行管理、飞行控制、通信导航等。核心软件将分区应用软件与硬件环境隔离开，同时也为应用软件的运行提供通信、调度等各种底层服务。一般来说，为了满足各种功能需求，IMA系统中的分区应用软件数量很多，而作为核心软件的操作系统往往只有一个，分区应用软件与核心软件间的信息传递是通过应用可执行接口(APplication/EXecutive，APEX)来实现的。

图1 ARINC653标准定义的IMA架构

ARINC653标准定义的IMA软件系统将分区作为其核心理念。模块被划分为若干个分区，并给每个分区分配了指定的内存空间和处理器时间片等资源。在此基础上，分区应用软件的各种功能可以通过调度部署在不同分区内的任务进程来实现。本文研究的IMA分区可调度性即为其中分区应用软件的关键特性。

1.2 分区调度机制

根据ARINC653标准，IMA系统中对于分区应用软件采用了双层调度机制，如图2所示。操作系统层进行分区层调度，分区调度器对处理器时间进行分派，以时间片轮转的方式来激活各分区。在此基础上，应用软件层进行任务层调度，各分区被激活后，其中的任务调度器按照配置好的策略来调度相应的任务集，从而完成各应用软件的功能。

图2 IMA分区应用软件的双层调度机制

(1) 分区层调度。分区层调度为上层调度机制，是指操作系统对各分区的调度。分区层调度机制如图3所示。

图3 IMA分区层调度

分区层调度采用了循环调度算法(Round-Robin，RR)，这是由系统配置文件所决定的，是固定不变的。如图3所示，分区之间没有优先级之分，在一个主时间框架内，所有分区都会至少分配到一个系统时间片，且每个分区获取系统时间片的周期和长度均为定值。

(2) 任务层调度。任务层调度为下层调度机制，是指在分区分派的时间片内对其内部的任务进程进行调度。

与分区层调度不同，任务层调度采用基于优先级的可抢占式调度策略，例如最早截止期优先算法(Earliest Deadline First，EDF)、时限单调调度算法(Deadline-Monotonic Scheduling，DMS)和速率单调调度算法(Rate-Monotonic Scheduling，RMS)等。在任务层调度中，每个任务都被赋予一个优先级，任务调度器始终将时间片分配给当前优先级最高的任务。如在任务执行期间，某一更高优先级任务被调度，则立即停止当前任务，执行高优先级任务，并在高优先级任务结束后再恢复执行当前任务。

综上所述，IMA系统的分区调度机制可概括为：操作系统将处理器时间片按照固定的周期和顺序分派给各分区；各分区下的任务进程则按照其自身优先级抢占分区时间片。需要注意的是，当某分区获得的处理器时间片截止时，其中的任务进程也会立即失去调度并暂停执行，直到该分区再次获取系统时间片后再恢复执行。

为了保证IMA系统的安全运行，各分区中任务的执行均应在其截至期限前完成，即需要具备充分的可调度性。然而，由于任务层调度中采用了优先级抢占式调度策略，各任务获取时间片的周期和长度是由其自身的约束条件(执行时间、截止时间、优先级)决定的，这极大提高了调度过程的复杂程度，系统的可调度性难以直接判定。本文即针对IMA系统的分区可调度性验证方法进行研究。

2 分区调度与AADL元素映射规则

本文提出的IMA分区可调度性验证方法是基于AADL建模语言所构建的体系结构模型实现的。因此，需首先建立IMA分区调度的主要概念与AADL中的各类组件、属性等建模元素之间的有效的语义映射。

AADL定义了3类组件：软件组件，包括数据(data)、线程(thread)、进程(process)和子程序(subprogram)；执行平台组件，包括处理器(processor)、虚处理器(virtual processor)、存储器(memory)、总线(bus)、虚总线(virtual bus)和外设(device)；系统组件可将所有的组件整合，层次化地建立系统的体系结构。为满足不同的应用需求，AADL还引入了附件的概念，如用于故障事件及属性建模的错误附件(Error model Annex)和用于实际功能行为建模的行为附件(Behavior Annex)。

结合IMA分区调度原理，本文建立的模型语义映射规则如表1所示。

表1 AADL与IMA分区调度的模型语义映射规则

AADL处理器组件可以描述分区和任务的执行环境，其与IMA分区调度中的操作系统概念相同。其中，考虑到各分区均需要独立的执行环境，因此通过虚处理器子组件将处理器组件分成相互独立的逻辑资源。

分区映射为AADL进程组件，且需将不同分区绑定相应的虚处理器子组件和内存组件。其中，内存组件用于描述执行分区的内存要求，并通过虚处理器子组件的属性来描述分区层调度策略。

AADL进程组件中往往包含一个或多个作为基本执行单元的线程组件，可以用来表示任务的执行，因此将任务映射为线程组件。

行为附件是AADL的延伸，其可以通过代码描述系统对分区中各任务的调度操作，因此将任务层调度策略映射为行为附件模型。

3 IMA分区可调度性验证模型

根据上述映射规则，本文建立了IMA系统分区的可调度性验证模型。在静态体系结构模型的基础上，通过建模其动态行为来描述任务调度过程，分别为分区架构模型和分区调度策略模型。

3.1 分区架构建模

为方便讨论，以用于实现大气数据温度传输的某应用软件的分区调度为例，阐述本文所提出的建模与验证方法，相关参数如表2所示。

表2 IMA系统分区参数

表2中给出了该系统在主时间框架为30 ms下的分区和分区内任务的调度情况。该系统含有P1和P2两个分区，其中所采用的任务层调度策略分别为DMS和RMS。P1和P2分配的时间片长度分别为20 ms和10 ms。两个分区中各包含2个任务，并规定了相应的周期、执行时间和截止时间。

根据第2节中提出的模型映射规则，构建该系统分区架构的AADL模型，如图4所示。

图4 分区架构AADL模型

图4中，IMA的操作系统由AADL处理器组件“CPU”描述，其中包含两个虚处理器子组件“Virtual_processor_P1”和“Virtual_processor_P2”。系统的两个分区分别用AADL进程组件“Partition1”和“Partition2”进行建模，并绑定到相应的虚处理器和内存，绑定关系由带箭头的虚线表示。分区中的各任务则分别映射为AADL线程组件“Order”、“Temperature_capture”、“Printer”、“Receiver”。此外，本文研究对象为IMA系统的分区和任务的调度，因此忽略任务间的数据传输，将其简化为事件触发<>，在图4中用实线表示。

3.2 分区调度策略建模

针对IMA系统的两层调度机制建立其分区调度策略的AADL模型。

(1) 分区层调度建模。由1.2节可知，IMA系统的分区层调度采用了RR调度算法，各分区按照固定周期轮流获取处理器时间片。根据表2中给出的主时钟框架周期和分区时间片，构建其分区层调度策略模型，如图5所示。

(a) 分区层调度策略 (b) 分区层调度策略模型图5 分区层调度策略建模

建模时通过AADL虚处理器子组件的3个属性来描述分区层调度策略。以分区1为例，在图5(b)中，“Dispatch_Protocol=>Periodic”表示采用周期固定的循环调度算法，“Period=>30 ms”定义分区调度周期即主时钟框架为30 ms，“Execution_Time=>20 ms”定义分区1所获取的处理器时间片为20 ms。

(2) 任务层调度建模。为解决现有方法不能有效描述IMA分区两层调度机制的问题，本文基于AADL的行为附件构建了任务层调度策略模型，并通过行为附件描述了分区内任务复杂的调度操作。

针对IMA系统任务层所采用的基于优先级的抢占式调度策略，并结合AADL行为附件的建模特性，设计相应的任务调度模型的执行流程如图6所示。

图6 任务调度模型的执行流程

由图6可知，当判定任务被调度后，系统将其置入任务队列，并在队列中按优先级对所有任务进行排序。在队列中处于首位的任务优先级最高，其将立即执行。任务执行完成后，系统会将其移出任务队列，等待下一次调度。另外，如果某任务运行时，系统调度了另一优先级更高的任务，则当前任务将暂停执行并挂起，直到其再次成为队列中优先级最高的任务时才能恢复执行。其中，判定当前任务执行过程中是否有更高优先级任务被调度的时间间隔设定为1 ms，其取自表2给出的各任务的调度周期和执行时间的最大公约数。针对不同分区参数，该值可根据情况做相应改变。

根据图6，基于AADL行为附件对分区中的全部任务分别建模，构建IMA系统任务层调度策略模型。以任务“Temperature_capture”为例，其伪代码如图7所示。

图7 基于AADL行为附件的任务层调度策略模型

图7中，在AADL线程组件“Temperature_capture”的属性中定义了该任务的调度周期和截止时间，其调度行为则通过AADL行为附件中定义的状态转换过程来进行描述。

其中，行为附件模型代码中的“states”部分定义了5个状态：“Initial”为起始待命状态，“WaitRun”表示任务被调度后的等待运行状态，“Running”为任务执行状态，“HangUp”表示任务被抢占后的挂起状态，“Complete”为任务执行完成状态。

“transitions”部分通过上述状态的转换来描述任务调度过程。其中为实现相应功能定义了3个子程序：“enqueue()”用于将任务置入队列并进行优先级排序，“priority_test()”用于判定该任务是否为当前最高优先级,“dequeue()”用于在任务执行结束后将其移出队列。

4 IMA分区可调度性验证

本文采用AADL Inspector工具，基于模型分析的方法对IMA分区的可调度性进行评估。AADL Inspector提供了一套模型分析平台，不仅可以验证AADL模型的静态结构，也可以基于处理器利用率对其动态行为进行分析。由于本文所建立的IMA分区可调度性验证模型中已经对其调度行为进行了描述，因此，与传统方法相比，在进行可调度性验证时就不需要再对模型进行二次转换。

4.1 架构正确性验证

对于模型架构正确性的验证主要考察其是否正确描述了IMA系统的航电分区架构以及是否符合AADL建模规则。本文通过AADL Inspector的静态分析工具对所建模型进行验证，将上述模型作为AADL Inspector的输入，分析结果如下所示。

图8为所建模型的统计声明，其中给出了系统模型的组件数量以及组件属性的统计。由图8中给出的结果可知，模型中的处理器组件、进程组件和线程组件的数量均与表2中规定的分区参数一致。

图8 模型统计声明

图9为调用逻辑模型处理算法(Logic Model Processing，LMP)对模型中建模规则一致性的验证结果。该结果表明模型无建模规则错误。

图9 规则一致性验证

图10为调用LMP算法对模型中的语法限制进行验证。该结果表明模型符合AADL语法规则，无语法错误。

图10 语法合法性验证

图11为对模型中组件元素的命名规则和名称引用是否正确进行验证。该结果表明模型无命名规则错误。

图11 命名正确性验证

图12为对模型是否符合ARINC653标准中规定的软件架构规则进行验证。该结果表明模型无ARINC653规则错误。

图12 ARINC653一致性验证

通过上述静态验证结果可知，本文方法构建的分区可调度性验证模型能够正确描述系统体系结构且符合相应建模规则。

4.2 可调度性验证

分区可调度性验证是本文关注的重点问题，主要考察IMA系统分区和任务是否满足可调度性。判定条件为：如果某任务在每一次被调度后都能在其自身约束条件规定的截止时间前执行完成，则判定该任务可调度，否则不可调度；如果某分区中的所有任务均可调度，则判定分区可调度，否则不可调度。

通过AADL Inspector的时间分析工具对所构建模型的动态行为进行仿真，可获得分区任务调度甘特图，仿真结果如图13所示。

图13 分区任务调度仿真甘特图

图13中，横轴为系统运行时间，每格为5 ms。第1行表示处理器工作状态，灰色部分表明其正在工作，其余为空闲。第2行和第5行分别表示分区1和分区2所获得的处理器时间片，以灰色部分表示，由图中可知分区1获得时间片为20 ms，分区2获得时间片为10 ms。第3行、第4行、第6行、第7行分别表示分区中的4个任务的执行情况，灰色表明任务处于等待执行状态，黑色表明任务正在执行。

由于分区1的调度策略为DMS，任务的优先级与其截止时间成反比，则根据表2中参数，任务“Order”的优先级高于“Temperature_capture”，所以仿真结果中“Order”优先获得处理器时间片，待其执行完成(3 ms)后，“Temperature_capture”才能执行，而在其完成(2 ms)后系统暂无任务执行，处于空闲状态。另外，由于“Temperature_capture”的调度周期为15 ms，在分区1所获得的1个处理器时间片下其将执行2次。

分区2采用的调度策略为RMS，任务的优先级与其周期成反比，则根据表2中参数，任务“Receiver”的优先级高于“Printer”，其余结论与分区1相同。

由图13给出的分区调度仿真结果可知，所有任务均可调度，故所有分区均可调度，则可判定该IMA分区系统满足可调度性要求。

为进一步验证本文方法的有效性，对表2中给出的分区参数进行修改，并再次验证系统的可调度性。

(1) 将分区1和分区2在一个主时钟框架下获得的处理器时间片分别改为30 ms和0 ms。此时由于分区2没有分配处理器时间，其中的任务将无法在截止时间前完成。仿真结果如图14所示。

图14 修改分区时间片后的仿真结果

由图14可知，分区1占用了全部的处理器时间片，其下的两个任务均能够按照时间约束条件正常执行，分区1满足可调度性。然而，由于分区2无法获得处理器时间片，其下的任务无法按照时间约束条件执行，仿真结果中出现了不可调度错误，在第6行、第7行以深灰色表示，提示分区2中的任务不可调度。由此可判定该IMA系统分区架构不满足可调度性，这是由于分区时间片配置不合理导致的，仿真结果与上述分析结论相符。

(2) 将任务“Order”的执行时间修改为22 ms。此时，该任务的执行时间超过了其所规定的截止时间(8 ms)，同时也超过了分区1所获得的处理器时间片(20 ms)。这不仅会导致该任务无法在规定截止时间前完成，也会对分区1内的另一任务的调度执行产生影响。仿真结果如图15所示。

图15 修改任务执行时间后的仿真结果

图15中分区1下的两个任务所在行出现了不可调度错误，表明分区1不满足可调度性。其中，任务“Order”出现调度错误的时间点为其开始执行后的8 ms处，这是因为其未能在规定截止时间前完成执行。任务“Temperature_capture”在0～20 ms时间段内出现调度错误的时间点为15 ms，这是因为其未能在再次被调度前完成上次调度的执行。另外，分区2及其下任务所在行未出现错误，说明其满足可调度性。仿真结果说明该IMA系统分区架构不满足可调度性，这是由于任务时间约束条件配置不合理导致的，仿真结果与上述分析结论相符。

通过上述验证过程可知，本文所提出的基于体系结构模型的IMA分区可调度性验证方法与实际相符，具备有效性。另外，由于只需一次性建模即可完成可调度性验证，与现有方法相比，在验证过程中避免了对AADL模型进行繁琐的二次转化。

5 结 语

本文以IMA系统软件分区架构为研究对象，提出了一种基于体系结构模型的分区可调度性验证方法。在建立IMA分区调度的主要概念与AADL语义映射规则的基础上，通过AADL标准建模组件和行为附件分别构建IMA系统分区架构模型和分区调度策略模型，并基于所建模型调用AADL Inspector工具，通过模型分析的方法对IMA系统软件分区可调度性进行验证。通过验证，可以及时发现分区调度配置中的错误，为保证系统安全性和可靠性提供方法支持。