基于AADL的综合航电分区系统可调度性判定

袁 翔,胡 军,2,马金晶,刘 雪

(1.南京航空航天大学计算机科学与技术学院,南京210016;

2.南京大学计算机软件新技术国家重点实验室,南京210093)

基于AADL的综合航电分区系统可调度性判定

袁 翔1,胡 军1,2,马金晶1,刘 雪1

(1.南京航空航天大学计算机科学与技术学院,南京210016;

2.南京大学计算机软件新技术国家重点实验室,南京210093)

综合模块化航电(IMA)系统中的分区系统提高了其可靠性和安全性,但在系统设计和实现过程中,应采用各种分析和验证方法确保系统的时间需求得到满足。为此,针对符合ARINC653规范的IMA系统,根据分区系统层级调度的特性,提出一种基于仿真的分区任务集可调度性判定方法。借助Cheddar工具及其自定义调度策略功能,使架构分析和设计语言(AADL)具有对分区系统进行建模的能力,并利用该工具对AADL模型进行仿真以判定系统的可调度性。实例分析结果表明,该方法能自动、准确、快速地进行可调度性判定,并以甘特图的方式绘制任务调度过程,得到直观、详细的结果。

综合模块化航电;ARINC653系统;分区系统;架构分析和设计语言;Cheddar工具;可调度性判定;仿真方法

1 概述

综合模块化航电(Integrated Modular Avionics, IMA)系统[1]是航空应用领域中的一类重要系统结构。ARINC653标准[2]定义了一种IMA软件体系结构,制定了操作系统层和应用软件层之间的标准接口(APEX)。标准满足ARINC653的IMA系统称为ARINC653系统。

ARINC653系统提出了分区操作系统的概念,用来提高航空电子系统的可靠性、高安全性。为保障系统的安全性和可靠性,在系统的设计和实现过程中,应采用各种分析、建模及验证方法对系统进行严格的检验,以保证系统在各种情况下的非功能需求和时间需求都能得到满足。为了精确管理时间资源,以达到强实时性要求,对系统进行可调度性分析相当必要。

架构分析和设计语言(Architecture Analysis and Design Language,AADL)[3]是一种针对嵌入式系统建模描述语言,可应用于航空嵌入式系统(ARINC653系统)的架构设计建模及分析[4]。Cheddar是一款实时调度分析工具[5],可应用于实时系统的时间性验证,同时支持对AADL模型表示的实时系统进行可调度性分析。

鉴于ARINC653分区调度系统具有层级性(分为两级调度),且目前支持多层级调度分析的方法和工具并不完善,本文提出一种基于AADL模型,使用Cheddar工具对ARINC653分区调度系统进行可调度性判定的方法。首先利用AADL模型和Cheddar关于AADL的扩展属性对分区系统进行建模,再通过Cheddar工具对生成的AADL模型进行可调度性判定。

2 背景知识

2.1 ARINC653

ARINC653是一种IMA软件体系结构,如图1所示,它包括如下层次结构:应用软件层,ARINC653系统结构层,实时操作系统层,硬件接口层和硬件层。系统的功能要求包括分区管理、进程管理、时间管理、存储器管理、分区内通信、分区间通信及健康监控等功能定义[2]。

图1 ARINC653软件体系结构

本文的研究重点在应用软件层,它按资源分配和功能将系统划分为数个模块,模块又划分为数个分区,分区内包含具体的任务进程。通过引入分区概念,将模块分为若干个分区,每个分区分配指定的内存空间和处理器时间片。

关于分区的时间调度方面,一个ARINC653系统模块中有若干分区,每个分区下对应着各自的任务集合。将系统处理器时间按时间片的方式分配给各个分区,各个分区下的任务集合在相应分派的时间片下运行,当时间片用完时暂停执行,直到下一个时间片的到来。不同于普通的系统调度模型,分区调度模型包含两级调度策略,如图2所示。

图2 ARINC653分区系统调度框架

(1)分区间调度。分区间的调度是第1级调度,调度周期是固定的。每个分区周期性地分配到处理器时间。

(2)分区内调度。分区内调度是第2级调度,指分区内进程间的调度。分区内调度是由操作系统根据分区的调度策略来对任务进程集进行时间分配。与分区间调度不同,它是可抢占式的调度策略,如最早截止期优先(EDF)、空闲时间优先(LLF)、速率单调调度(RMS)、截止时间单调调度(DMS)等。每个任务具体分配到的时间片是无法通过配置来指定的,因此,无法直接判定每个任务是否都能满足它的可调度性。

在调度系统中,如果一个任务在每次到达之后都能在其截止时间限内执行完成,则判定该任务可调度,否则该任务不可调度。从而对任务可调度性的判定即对任务在截止时间期限内是否执行完成的判定。如果ARINC653分区系统中的所有任务都能在各自的截止时间限内执行完成,则判定分区系统可调度,否则,判定分区系统不可调度。本文即针对分区系统的可调度性判定方法进行研究。

2.2 AADL

AADL用于设计和分析系统的软硬件结构,包括独立的组件和它们的交互,尤其适用于性能关键的实时嵌入式系统。AADL的组件包括软件类、执行平台类和系统类。软件类包含数据、子程序、线程、线程组、进程5类组件;执行平台类包含处理器、存储器、设备、总线4类组件;系统类的系统组件是作为软件类组件和执行平台类组件的集成组件而设计的[3]。

本节将重点介绍AADL的线程、进程和处理器组件,因为这些组件将运用到ARINC653调度模型的建模。AADL的线程组件是一段执行程序段,这些程序段可以使用Ada任务来表示。根据任务的激活模式,线程类型可以分为周期线程、非周期线程、零星线程。周期线程在固定的时间间隔下被激活,这个固定的时间间隔称为周期,非周期线程在系统的任何时间被激活,没有任何规律性,零星线程在一个最小的时间间隔下被激活。AADL的进程组件提供了虚拟的时间和地址空间,每个进程下的需求资源都是独立和隔离的。AADL的处理器组件提供了线程运行的需求资源。线程、进程和处理器组件将用于对ARINC653系统分区调度中任务进程、分区、模块的建模。

AADL规范介绍了组件连接和组件属性。组件连接对组件之间的关系进行建模,如线程组件之间的时间同步、消息交互、共享数据访问。组件属性则存储着组件自身的一些信息,这些属性决定了组件在系统中的行为。组件属性包含名字、值、类型3个部分,如线程组件有属性Period,其值就是大于0的数,类型是整型。这个属性指明了周期线程的周期值。AADL包含标准的属性,这些属性不需要再进行声明。同时,为了满足特有的建模需求,允许第三方扩展相应的属性。本文的研究就是基于Cheddar的扩展属性集(详见文献[6]),依赖于这些扩展属性集,使用AADL对ARINC653系统进行建模,然后使用Cheddar工具对生成的模型进行可调度性分析。

2.3 Cheddar

Cheddar是一个免费的实时调度工具,专用于检查实时系统中的任务时间约束[5]。借助于Ocarina[7],它可以用来分析AADL模型的可调度性。Cheddar提供了一套类Ada语言(Cheddar语言[6]),使用这个语言可以设计用户自定义的调度策略。正是基于Cheddar的调度策略的可扩展性,可以使用AADL对ARINC653分区调度系统进行建模,同时使用Cheddar工具进行分区调度的可调度性分析。

Cheddar提供2种调度分析功能:可行性测试和仿真。可行性测试允许用户不进行调度模拟,根据已有的调度理论,研究实时应用程序、系统是否可调度。相反,仿真首先进行调度模拟,其次根据任务的约束属性判断任务的可调度性。可行性测试是简单不复杂的,文献[8]介绍了在几种经典调度策略下进行可行性测试的方法。不过,由于多层级调度策略的复杂性,当前还没有相应的可行性测试的方法。ARINC653系统是分区系统,采用的是多层级的调度策略,本文根据自主设计的调度策略,通过仿真的方法对多层级调度系统进行可调度性分析和判定。

3 相关工作

目前,安全关键系统已经广泛应用于许多安全领域,如航空航天、汽车、医药等领域,同时,这也导致系统越来越复杂。ARINC653就是一种航空电子设备标准,它提供了一种时间和空间隔离的分区方式,来提高系统的安全性。

为避免系统中的错误带来严重的后果,文献[9-10]介绍了几种方法用来检测安全关键系统的潜质错误。不过这些方法依赖于不同的符号和语言,在整个开发阶段无法统一,所以基于模型驱动的安全系统的分析方法被提出来[11]。使用模型驱动的方法分析安全系统已经被应用在多个项目中(Flex-eWare[12], SAVI[13])。

关于安全关键系统的AADL模型的可调度性分析方面,本文所使用的Cheddar就是一款实现调度分析工具,它可以根据EDF或EMS等经典调度策略公式,基于处理器利用率进行可调性判定[14]。文献[15]提出了使用进程代数ACSR来对AADL模型元素的子集来进行调度分析。由于ACSR方法的限制过多,其实用性并不高。TIMES[16]是基于任务自动机的调度分析工具,由于它的非周期线程的定义与AADL中非周期线程的语义并不一致,因此不能用于分析包含非周期线程的 AADL模型。文献[17]讨论了AADL模型到时间自动机的转换,并提出了使用UPPAAL工具进行可调度验证的方法。

针对分区系统的可调度判定的研究,文献[18]在任务时间需求函数的基础上,计算系统消耗时间,得出了系统可调度性的判定定理。文献[19]分析了分区参数对任务调度实时性的影响,针对周期和零星任务,通过计算任务的响应时间上界,推导出分区调度下的任务可调度条件。文献[20]设计并实现了时间分析工具IMATime,对分区系统FCOS进行三级分析,同时提供分区周期和分区容限。

4 基于AADL的ARINC653分区系统建模方法

使用Cheddar对ARINC653分区系统进行可调度分析前,必须先使用AADL对系统进行建模,本节将介绍借助于Cheddar扩展属性,如何使用AADL对 ARINC653分区系统进行建模。为使AADL能对ARINC653系统进行建模,必须找出AADL模型元素与ARINC653系统概念的对应关系。本节将介绍调度方面的对应规则以及Cheddar扩展属性的应用,同时给出如何在Cheddar中自定义调度策略,并根据上述的对应规则给出一个分区系统建模实例。

4.1 AADL与ARINC653的对应规则

4.1.1 模块对应规则

考虑到ARINC653系统模块包含一个或多个航空电子应用软件,并保证这些应用软件之间相互独立运行。系统将运行在模块上的多个应用软件按功能划分为多个分区,同时指明每个分区分配的系统资源和分区内的调度信息。而AADL中的processor组件可以用来指明系统运行时的执行环境,包括CPU的调度分配、内存分配、通信连接总线等。因此,可以使用AADL的processor组件表示ARINC653模块概念,这个组件提供了模块运行时的资源需求以及空间和时间隔离。同时,分区间的调度策略可以通过属性Dispatch_Protocol定义。由于分区系统调度的复杂性,当前并不存在一个已有的调度策略,因此需要借助于Cheddar属性自定义调度策略。首先processor组件属性Cheddar_Properties::Scheduling_Protocol需要赋值为AUTOMATA_USER_DEFINED_PROTOCOL,其次属性Cheddar_Properties::Source_Text赋值为包含调度策略的文件名,最后属性 Cheddar_Properties:: Automaton_Name赋值为调度策略所使用的时间自动机的名字。具体的自定义调度策略的方法流程见本文4.2节和4.3节。

4.1.2 分区对应规则

ARINC653分区包含了一组任务集合,它在时间和空间上是隔离的,不同分区的任务的运行是不受影响的。分区可以拥有不同的关键级别来保证分区间的数据流通的安全性。在模块的总时间框架内,分区被调度的周期和被分配的时间片是固定的,同时,基于空间隔离的需求,分区被分配在不同的地址空间里。考虑到AADL中的virtual processor组件可以用来构建一个逻辑资源,概念上是processor组件的一个子组件,可以将processor组件指明的运行环境分成多个互不影响的区域。每个逻辑资源可以单独指明相应的调度信息以及内存分配情况等。此外,AADL另一组件类型process组件,它指明了具体的执行条件,程序段和交互数据,它包含一个thread组件来表示执行的动作。因此,可以用AADL中的以上2种组件来表示ARINC653模块中分区概念,其中virtual processor组件指明分区运行时资源的分配(任务调度,分区资源等),而process组件指明了分区包含的内容(线程、数据等)。这2种组件之间的关联通过 AADL属性 Actual_Processor_ Binding定义。processor组件包含一组 virtual processor组件,如同模块包含一组分区。

分区内调度策略的定义方法与上述介绍的模块下分区间调度策略类似,本文不再详述。

4.1.3 进程对应规则

ARINC653进程是系统执行主体,它包含了执行代码、执行数据和堆栈区域等。一个分区可以包含多个进程,来实现相应的应用功能。分区通过指明进程的调度策略、抢占策略、最大响应时间、内存分配情况等信息来控制进程的执行。而AADL中的thread组件是系统最基本的调度执行单元,通过时间周期或者外部事件来执行线程。线程间的通信可以通过端口连接、子程序调用和共享数据来实现。因此,可以使用AADL的thread组件表示ARINC653进程概念,因为它们有相同的概念:执行主体。执行主体所需要的特征可以用AADL属性来定义,包括执行周期、执行截止时间、执行时间和调度策略等。AADL中的thread组件包含在process组件中就像ARINC653中的进程包含在分区中一样。thread组件属性Dispatch_Protocol定义线程类型即激活模式(如周期、非周期、零星等),Compute_Execution_ Time定义线程的执行时间,Period定义周期线程的周期值,Deadline定义线程最坏响应时间。

图3总结了上述的对应规则,即给出了使用AADL中的哪些组件和属性对ARINC653系统分区调度信息进行建模。比如使用AADL中的处理器组件给ARINC653中的模块建模,其中使用组件属性Thread_Properties::Scheduling_Protocol表示模块下分区所采用的调度策略。依赖于表格中的AADL标准属性和以Cheddar_Properties::开头的Cheddar扩展属性生成的AADL模型,Cheddar工具就可以进一步进行可调度性分析和判定。

图3 AADL与ARINC653对应规则

4.2 Cheddar自定义调度策略

使用Cheddar语言定义一个新的调度策略,它由两部分组成:类Ada语言程序段和时间自动机。类Ada语言程序段用来进行仿真计算,同时它也提供了必要的仿真数据(如任务周期、任务唤醒时间、任务优先级、任务截止时间等)。程序段被分为多个部分,分别在仿真的不同阶段进行模拟计算,这些部分包括:start_section,包含变量的声明和初始化; priority_section,在每个单元时间片分配前,计算每个任务的优先级;election_section,指定下一个单元时间片分配给的任务。

使用Cheddar语言定义的调度策略Ada程序段如下:

上述3个程序段都有相应的命名。首先在start_ section片段内定义了一个数组dynamic_priority,系统初始化时,创建大小是任务个数的数组。再在priority_section片段内将上述数组赋值为任务集的周期值数组,那么在时间片分配前,dynamic_priority数组保存着当前任务集的周期值,最后在election_ section片段内返回dynamic_priority数组中值最小的索引,即返回周期值最短的任务索引(min_to_ index是Cheddar工具自带的内嵌函数,用来返回数组中值最小的索引)。根据上述定义的调度策略,它与RMS调度策略比较相似,周期值越小的任务优先分配到时间片。

时间自动机用来表示线程状态的时间转换情况,可以用实时系统验证工具UPPAAL生成。使用时间自动机的节点,时间约束和变量值表示系统的状态。每个时间自动机的转换可以是独立的,也可以与其他的时间自动机同步进行状态转换。使用时间自动机来表示任务的运行和切换,使用时间约束来控制状态转换过程。Cheddar使用时间自动机对线程调度进行建模,并运行上述的类Ada语言程序段,读写仿真数据。

在Cheddar中定义的一个时间自动机的代码示例如下:

首先定义一个状态Ready,即自动机的初始化状态,再定义一个状态迁移关系,从状态Ready迁移到状态Ready,即系统都处在状态Ready。状态转换包含3个部分:变量更新,判定条件,同步信号,该示例中变量更新和判定条件是没有的,不过存在一个同步信号。当处在Ready状态的线程接收到election_ name同步信号(上文Ada程序段中election_section调度完毕后系统会发出election_name信号)时,会发生状态迁移,状态再次迁移到Ready。

针对分区调度系统,通过定义2种不同的调度策略,一种用于分区间调度,另一种用于分区内任务调度。2种调度策略之间通过同步信号来同步和交互,完成多层级调度,具体见下节的建模实例分析。

4.3 建模实例分析

本节将给出一个建模的例子,介绍如何借助于Cheddar扩展属性,使用AADL对ARINC653系统的分区调度模型进行建模,建模流程如图4所示。首先根据系统的调度信息,使用Cheddar设计相应的调度策略,其次依赖于 4.1节介绍的 AADL与ARINC653的对应规则和调度策略,分别使用AADL的thread组件、process组件和processor组件对系统中的进程、分区、模块建模,同时,将设计好的调度策略赋予组件属性。

图4 ARINC653分区系统建模过程

表1是ARINC653系统分区间和分区内的调度信息,详细描述了一个总时间框架下(时间片大小是10 ms)分区集和各分区任务集的调度情况。系统包含有2个分区(partion1和partion2),每个分区包含有2个任务,调度策略分别是DMS和RMS。

表1 ARINC653系统调度信息 ms

使用AADL对上述ARINC653分区系统调度信息进行建模,得到模型如下:

AADL的 processor组件(arinc.Impl)表示ARINC653系统分区运行所在的模块(arinc),2个AADL的 process组件(partition1.Impl和 partition2. Impl)表示ARINC653系统中的2个分区(partiton1和partition2),4个AADL的thread组件表示ARINC653系统中的4个任务进程。每个分区分别包含2个任务进程(partition1包含T1和T2,partition2包含T3和T4),Actual_Processor_Binding属性将进程组件与处理器组件绑定,指明进程所在的处理器组件。进程partition1和partition2所在的执行组件都是arinc.Impl,即ARINC653系统中2个分区同在arinc模块中。

AADL属性Compute_Execution_Time,Dispatch_ Protocol、Period、Deadline等指明了ARINC653系统任务的调度信息,其中,Compute_Execution_Time, Dispatch_Protocol、Period、Deadline等是AADL的标准属性,指明了任务的执行时间、任务的类型、周期任务的周期时间、任务的截止时间等。

AADL扩展属性Cheddar_Properties::Scheduling_ Protocol指明调度策略,例子中处理器和2个进程组件都有独立的调度策略,分别定义了模块下分区间的调度策略和分区partion1和partion2内的调度策略。模型中arinc.Impl处 理器 组 件 的 Cheddar_Properties:: Scheduling_Protocol属性值是AUTOMATA_USER_ DEFINED_PROTOCOL指明了分区间的调度策略是Cheddar自定义的时间自动机,使用时间自动机表示线程的状态转移情况。Cheddar_Properties::Source_Text属性值指明了时间自动机所在的文件名,arinc_ processor.sc包含了分区间调度的Cheddar程序段和时间自动机。partition1和partition2进程组件属性值与处理器组件相同,不过调度策略所在的文件不同。arinc_ partition1.sc和arinc partition2.sc文件分别包含了这2个分区的调度策略。

arinc_partition1.sc文件包含了图5(a)所描述的时间自动机。partition1_capacity变量指明分区partition1在一个总时间框架内被分配到的时间片大小,partition1_duration变量指明分区已经执行的时间片大小。在程序段election_section内,根据DMS调度策略的定义,指定下个时间片将分配给截止时间最小的任务。这里调用了Cheddar内嵌函数min_to_ index来获取当前处于等待状态并拥有最小截止时间的任务,文献[6]详细介绍了Cheddar的内嵌函数。arinc_partition2.sc文件包含了图5(b)所描述的时间自动机,变量定义也是一样的。由于调度策略的不同,这个分区使用的是RMS调度策略。在程序段priority_section内,根据RMS调度策略的定义,指定下个时间片将分配给周期最小的任务。arinc_ processor.sc文件包含了图5(c)所描述的分区间调度时间自动机,指明在10 ms总时间框架下先分配6 ms给分区partition1,再分配4 ms给分区partition2,如此周期性的时间片分配。

图5 调度时间自动机

文本内容基本相似,本文不再赘述。

5 基于Cheddar的可调度性判定

本文针对含有纯周期任务的分区系统的可调度性判定问题,提出一种基于仿真方法实现的可调度性判定方法,具体流程如图6所示。该方法通过设定时钟变量来模拟任务调度过程中的系统时钟,在时钟变量值增长过程中,根据任务优先级从高到低的顺序分析各个任务约束属性的满足情况,判定任务的可调度性,从而判定分区系统的可调度性。

图6 可调度性判定流程

由于分区系统下调度模型的多样性,以及本文提出的可调度性分析方法的局限性,需要对调度模型进行限制。下文将介绍可进行可调度判定的分区调度模型和进行可调度性判定方法的理论依据,并给出基于上述描述的分区系统进行可调度性判定的实例。

5.1 ARINC653分区系统的调度模型

ARINC653分区系统相应调度模型描述如下: (1)系统中有若干个分区,分区间可以进行通信,但分区之间在时间和空间上彼此独立。

(2)系统为各分区分派时间片,各分区的时间片都有时间片开始时间(offset)和时间片大小(duration)2个参数,系统周期性地为分区分派时间片。

(3)系统可为各分区设定相互独立的分区内任务集调度策略。

(4)各分区内的任务集在各自分区分派的时间片内按照相应的调度策略调度执行,不受其他分区任务的干扰,任务集在执行过程中遇到时间片用完时,暂停执行过程,等待下一个时间片的到达。

(5)分区下的所有任务都是周期任务,且任务的周期等于任务的截止时间,具有硬实时系统的强时间限定,即必须在各任务的截止时间内完成,否则分区任务集不可调度。

(6)调度中忽略任务间切换的时间。

(7)分区下的任务是可抢占的,且在同一处理器下运行。

(8)只针对时间约束分析,默认任务所需的其他非时间资源都满足要求。任务的可调度性判定等价于判定任务的时间约束是否满足。

5.2 理论依据

针对非分区系统的调度模型,任务集下的所有任务都是周期任务,且各个任务的分派到达仅依赖于其相应的周期。因此,任务第一次到达以后的所有到达时刻都是确定的,用设定系统时钟变量来模拟调度过程的方法是可行的。

假设任务集s含有n个周期任务,设定n个任务都在0时刻到达,这n个任务下一次同时到达的时刻为此n个任务周期值的最小公倍数的时刻。n个周期任务的到达在整体上也呈周期性,且周期值为所有任务周期值的最小公倍数,文献[21]给出了相关证明。

针对分区系统和上述限定的调度模型,分区周期性获得系统分派的时间片。各分区下任务集中所有任务都是周期任务,因此,所有任务的触发到达呈周期性。在分区调度模型中,所有任务的到达执行与所在分区的时间片分派情况整体上呈周期性,周期值为所有任务周期值与分区获得时间片的周期值的最小公倍数。

依据上述周期最小公倍数理论可知,任务的执行过程呈周期性往复执行,因此本文在用仿真方法模拟任务调度过程判定任务集的可调度性的实现过程中,将系统时钟设定为一个周期值的时钟区域,分析任务集在此周期内的调度情况,从而等价描述系统时钟中剩余时间区域的可调度情况。因为任务执行过程中的确定性和周期性,所以系统时钟的选取是确定的有穷的时钟区域,因此,用仿真方法判定分区调度模型的可调度性是可行的。

5.3 仿真实例分析

表1描述了分区系统的任务调度信息,系统包含4个周期任务且周期等于截止时间。调度信息满足上述的可进行可调度性判定的调度模型。这4个周期任务的周期分别是10 ms,5 ms,20 ms,10 ms,最小公倍数是20 ms,分区获得时间片的周期是10 ms,所以所有任务周期与分区获得时间片的周期的最小公倍数是20 ms,即仿真时长是20 ms。

根据第4节介绍的内容,将包含表1分区调度信息的AADL模型作为Cheddar工具的输入,同时,编辑好自定义的调度策略,设置好仿真时长,调度结果如图7所示。

图7 调度仿真结果

可调度性判定结果分为上下2个部分,上面是任务在仿真时长内的调度甘特图,下面是判定结果。调度图中的一小格代表一个时间片,在本例中是1 ms。分区获得时间的周期是10 ms,分区partition1包含任务T1和T2,它被首先分配到6 ms的系统时钟,此时分区partition2中任务是空闲不运行的。由于分区partition1的调度策略是DMS,任务的截止时间与优先级成反比,而任务T1的截止时间大于T2的,所以T2的优先级大于T1。T2优先获得系统时钟,当T2完成它的任务后(执行时间1 ms),T1再获得系统时钟。当T1完成它的任务(执行时间3 ms),分区partiton1共执行了4 ms的时间,在之后的一个时间片上,由于partiton1里没有任务可运行,partiton2还没有被分配到系统时钟,系统处于空闲状态。在第6 ms时刻,周期为5 ms的任务T1再次被分配到1 ms的时间片。当T1执行完这个时间片后,分区partiton1的执行时间达到了6 ms,系统将把下一个时间片分配给分区partiton2。分区partition2包含任务T3和T4,由于分区partition2的调度策略是RMS,任务的优先级跟任务的周期成反比。T3的周期大于T4的周期,因此T4的优先级大于T3的优先级。T4将会先被分配到系统时钟,执行完任务后(执行时间2 ms),T3再获得系统时钟,也执行完任务(执行时间2 ms)。分区partition2共执行了4 ms时间,此时系统执行时间达到10 ms,下个时间片,系统再次将系统时钟分配给分区partiton1。不过在这个周期内,由于T3的周期是20 ms,它将不会被激活和分配系统时间片。综上所述,系统将以20 ms为周期,周期性地进行时间片的分配。

调度结果图中下半部分给出了可调度性判定,判定结果是可调度的,同时列出了每个任务的最坏响应时间,满足任务的截止时间要求。

6 结束语

为满足航空电子系统高可靠性、高安全性的需求,ARINC组织发布了航空电子应用软件标准接口ARINC653。目前ARINC653标准中提出的分区操作系统架构已经成为航空电子系统的新标准。航空电子系统对实时性要求极高,因此,对系统进行时间调度验证是有必要的。针对ARINC653系统的分区概念的特性,本文提出了一种对分区任务集进行可调度性判定的方法。本文使用建模语言AADL对ARINC653系统进行建模,通过Cheddar扩展属性和自定义调度策略,使得Cheddar具有对分区系统进行可调度性判定的能力。Cheddar提供了一种类Ada语言(Cheddar语言),通过一组程序段和时间自动机来设计分区调度策略,再通过仿真的方式模拟系统时钟的执行,根据仿真结果判定系统的可调度性。在使用本文方法对分区系统进行可调度性判定时,对分区下的任务有许多限制。任务必须是周期线程,且周期值等于截止时间等一些限定条件,限制了本文方法的使用场景。对于带有非周期性任务的分区,即不满足限定条件的任务,如何进行可调度性判定是下一步的研究方向。

[1] 易建平,韩 庆.飞机综合模块化航电系统总体设计研究[J].科学技术与工程,2010,10(19):2709-2714.

[2] AeronauticalRadio,Inc..ARINC Specification 653 Avionics Application Software Standard Interface[Z]. 1997.

[3] AADL Portal at Telecom ParisTech(AADL)[EB/OL]. (2009-07-14).http://aadl.telecom-paristech.fr/.

[4] Delange J,Gilles O.Model-Based Engineering for the Development of ARINC653 Architectures[J].SAE International Journal of Aerospace,2009,3(1):79-86.

[5] Singhoff F,Legrand J,Nana L.Cheddar:A Flexible Real Time Scheduling Framework[C]//Proc.of International ACM SIGAda Conference.Atlanta,USA:[s.n.],2004: 1-10

[6] Singhoff F.Cheddar Release 2.x User’s Guide[R]. Technical Report:singhoff-01-07,2007.

[7] TELECOM ParisTech,Inc..Ocarina User Guide[Z]. 2005.

[8] Stankovic J A,Spuri M,Natale D M,et al.Implications of Classical Scheduling Results For Real Time Systems [J].IEEE Computer,1995,28(6):16-25.

[9] Atchison B,Lindsay P.Safety Validation of Embedded Control Software Using Z Animation[C]//Proc.of the 5th IEEE International Symposium on High Assurance Systems Engineering.Albuquerque,USA:IEEE Press, 2000:228-237.

[10] Conmy P,Nicholson M,McDermid J.Safety Assurance Contracts for Integrated Modular Avionics[C]//Proc.of the 8th Australian Workshop on Safety Critical Systems and Software.Canberra,Australian:[s.n.],2003:6978.

[11] Kashi R N,Amarnathan M.Perspectives on the Use of Model Based Development Approach for Safety Critical Avionics Software Development[C]//Proc. of International Conference on AerospaceScience and Technology.Bangaloire,India:[s.n.],2008.

[12] Delange J,Hugues J,Pautet L,et al.Code Generation strategies from AADL Architectural Descriptions Targeting the High Integrity Domain[C]//Proc of the 4th EuropeanCongressERTSEmbeddedReal-time Software.Toulouse,France:[s.n.],2008.

[13] Chilenski J. Aerospace Vehicle Systems Institute Systems and Software Integration Verification Overview [C]//Proc.of AADL Safety and Security Modeling Meeting.[S.l.]:IEEE Press,2007.

[14] Singhoff F,Legrand J,Nana L.Scheduling and Memory Requirements Analysis with AADL[J].Ada Letters, 2005,25(4):1-10.

[15] Bremond G P,Choi J Y,Clarke D,et al.A Process Algebra to the Schedulability Analysis of Real-time Systems[M].Norwell,USA:KluwerAcademic Publishers,1998.

[16] Amnell T,Fersman E,Mokrushin L,et al.TIMES——A Tool for Modeling and Implementation of Embedded Systems[C]//Proc.of the 8th International Conference on Tools and Algorithms for the Construction and Analysis of Systems.London,UK:Springer-Verlag, 2002:460-464.

[17] 李振松,顾 斌.基于UPPAAL的AADL行为模型验证方法研究[J].计算机科学,2012,39(2):159-161.

[18] 何 峰,宋丽茹,熊华钢.航空电子双层任务分区调度设计[J].北京航空航天大学学报,2008,34(11): 1364-1368.

[19] 周天然,熊华钢.航空电子系统混合实时任务的双层调度[J].航空学报,2011,32(6):1067-1074.

[20] 汤小明,张新国.基于分区的安全关键软件体系及其时间分析研究[J].系统仿真学报,2013,25(7): 1704-1709.

[21] Leung J,Merrill M L.A Note on Preemptive Scheduling of Periodic Real-time Tasks[J].Information Processing Letters,1980,11(3):115-118.

编辑 金胡考

Schedulability Determination of Integrated Modular Avionics Partitioned System Based on AADL

YUAN Xiang1,HU Jun1,2,MA Jin-jing1,LIU Xue1
(1.College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 210016,China;
2.State Key Laboratory for Novel Software Technology,Nanjing University,Nanjing 210093,China)

Integrated Modular Avionics(IMA)partitioned system is put forward to improve the reliability and security of the system,but in the process of system design and implementation,analysis and validation should be used to ensure that the system time requirements are met.In allusion to IMA system which meets ARINC653 specification,according to the characteristics of hierarchy scheduling partitioned system,this paper proposes a schedulability determination method based on simulation method.With the aid of Cheddar tool and the function of custom scheduling strategy,Architecture Analysis and Design Language(AADL)has the ability of modeling partitioned system,then the tool operates on the generated AADL model to determine the system schedulable.Example analysis result shows that the tool has automatic, accurate and fast advantages to describe task scheduling process by Gantt chart and the result is accurate and detailed.

Integrated Modular Avionics(IMA);ARINC653 system;partitioned system;Architecture Analysis and Design Language(AADL);Cheddar tool;schedulability determination;simulation method

1000-3428(2014)10-0052-09

A

TP311

10.3969/j.issn.1000-3428.2014.10.011

国家自然科学基金资助项目(61272083);江苏省普通高校研究生科研创新计划基金资助项目(CXZZ11_0218)。

袁 翔(1987-),男,硕士研究生,主研方向:嵌入式软件建模与分析;胡 军,副教授、CCF会员;马金晶、刘 雪,硕士研究生。

2013-08-27

2013-11-08E-mail:yuanxiangnuaa@163.com

中文引用格式:袁 翔,胡 军,马金晶,等.基于AADL的综合航电分区系统可调度性判定[J].计算机工程, 2014,40(10):52-60.

英文引用格式:Yuan Xiang,Hu Jun,Ma Jinjing,et al.Schedulability Determination of Integrated Modular Avionics Partitioned System Based on AADL[J].Computer Engineering,2014,40(10):52-60.