基于时间自动机的嵌入式系统AADL 模型可调度性验证

李 静 沈宁敏 白海洋 周培云

(南京航空航天大学计算机科学与技术学院，南京211106)

伴随微电子、通信等技术的飞速发展，嵌入式实时系统广泛应用于航空航天、工业控制等任务的关键领域中，为了提升系统开发效率和可靠性，基于模型驱动架构(model driven architecture，MDA)［1］思想的体系结构分析与设计语言AADL被应用到嵌入式实时系统的建模与模型验证中.它能更好地支持嵌入式系统软硬件一体化的建模，同时对系统的可靠性等非功能属性进行描述［2］.其中，可调度性是指系统的调度策略和资源状况能否满足所有任务的执行需求，在任务的截止时间之内完成执行且不发生死锁，是嵌入式实时系统正确执行的最基本性质.

AADL 模型验证与分析主要采用仿真和形式化方法.ADeS 作为一种系统行为的仿真工具，目前还不支持子程序调用、行为附件的仿真［3］.Singhoff 等［4］采用仿真方法对可调度性进行分析，但处理复杂模型时效果不佳.Gui 等［5］结合进程代数理论对AADL 模型的组件进行分析，但仅支持比较简单的调度模型.形式化方法能够更精确地研究系统特性，AADL 属于高层建模语言，需要将其转换为较低层次的形式化模型，实现实时系统的研究与相关验证工具的有效结合［6-8］.AADL2BIP［9］工具能将AADL 模型转换成BIP 语言，使用验证工具VERSA［10］对其进行验证，但支持的调度类型较少.Hugues 等［11］将AADL 模型转换成Petri 模型进行形式化验证.Johnsen［12］利用UPPAAL 工具建立了时间自动机模型，支持基本固定优先级的调度策略模拟与验证.

本文借助时间自动机(timed automata，TA)的形式化验证手段，通过模型转换的方法将AADL调度模型转换到时间自动机模型，并利用UPPAAL 工具对原模型进行等价验证.

1 模型分析与语义转换

AADL 模型文件被自动转换插件解析后，根据语义规则将AADL 的元素映射成时间自动机中对应的元素，形成时间自动机模型.然后，利用UPPAAL 工具对生成的时间自动机模型进行性质验证.该方法的核心是构建出不同调度策略的时间自动机模型以及AADL 模型到时间自动机模型的映射法则(见图1).

图1 AADL 模型可调度性验证方法框架

1.1 AADL 模型

AADL 调度模型定义为一个四元组S=〈R，Z，TP，Q〉.其中，R 为处理器组件，其定义的属性集包含了处理器的特性，且调度模型中主要关注Thread-Limit(线程限制个数)与Scheduling-Protocol(调度策略)两个属性，前者设定了绑定在一个处理器上的最大线程数量，后者则规定了处理器调度策略;Z 为进程组件，使用Allowed-Processor-Binding(允许处理器绑定)与Actual-Processor-Binding(实际处理器绑定)来绑定处理器，且可通过属性和子组件定义的方式，在进程组件中定义线程子组件，并将进程作为管理单元关联起任务和任务的执行单元;TP为线程集合;Q 为端口之间的连接.令ti为第i 个线程，则ti=〈x，f，p，e，m〉.其中，x∈N 为线程标识符;f 为绑定于线程的数据端口，包含输入端口和输出端口;p 为与调度策略相关的属性集合，包括线程派发策略Dispatch-Protocol、线程时钟周期P、线程执行时间W、约定的截止时间D 和线程的优先级F;e 为模式状态，主要配合行为模型定义系统的不同状态集合;m 为行为模型，定义了线程的详细动作，是对执行模型的扩展.

1.2 时间自动机模型

一个时间自动机可以表示为一个六元组A=〈L，l0，C，V，E，I〉.其中，L 为有穷状态集合;l0为初始状态;C 为有穷时钟集合;V 为同步标号(时间或指定信息)的有穷集合;E∈L ×V ×φ(C)×2C×L为转移集合;I:L→φ(C)表示L 中的位置赋以某个时钟约束，此时钟约束即称为位置不变式.

一个时间自动机A 的语义可以通过与时间系统相关的转移系统SA进行定义，用二元组〈l，ν〉来表示，其中l∈L 为A 的某一状态，ν 为满足不变式I(l)的某一时钟解释.若l=l0，在该初始位置上所有时钟变量的初值为0.

SA包括2 种类型的迁移:①延迟迁移.状态因时间流逝而发生的改变，即其中δ≥0 为实数值时间增量，ν∈I(l)，且ν + δ∈I(l).②位置迁移.状态因位置转移而改变，即满足的条件，发生由状态l 到l'的迁移，且ν∈I(l)，ν'∈I(l')，其中g，a，u 分别为守卫条件、同步通道和更新操作的集合.

1.3 AADL 调度模型到时间自动机模型的语义转换

建立AADL 调度模型到时间自动机的语义映射，将处理器组件与各个线程分别映射为一个时间自动机，从而建立起一个调度模型的时间自动机网络.定义转换规则Γ(A)=〈B，N，K〉.其中，B 为时间自动机网络中的自动机集合;N={x，sch-info}为映射中全局变量，表示线程标号和线程属性信息;K={派发，运行，完成，错误}为全局同步通道信号.

AADL 模型到时间自动机模型的转换映射主要包括以下2 种:

1)线程组件到时间自动机的映射.即Bi+1=各线程分别转换到一个时间自动机用于表示执行状态的切换.其中，转换规则ΓG:G→A 将线程的语义映射到时间自动机模型语义.ΓG(ti)的转换对应ti→〈L，l0，C，V，E，I〉.其中，映射法则的语义已明确，需建立具体的映射法则来确定A 语义中的具体内容.线程的基本状态映射为A 的初始化、就绪、执行、出错和被抢占5个状态，即L={初始化，准备，运行，错误，抢占}.此时，C={k}为控制线程派发和记录线程截止时间的时钟;V={P，W，D，F}用于记录时钟周期P、执行时间W、截止时间D 和优先级的整型变量F.E={初始→准备，准备→运行，运行→初始化，初始→准备，运行→错误，g，a，u}为不同状态之间的转移;I(l0)={k≤P}.这里仅给出了周期线程在初始状态上的不变条件，对于非周期线程，状态转移由同步通道触发.

2)处理器组件到时间自动机的映射.即B0=ΓR(R)，ΓR(R):R→A，将处理器组件及调度相关模型映射到一个时间自动机.转换的规则为ΓR(R)=〈L，l0，C，V，E，I〉.此处，L={等待，调度器，运行，抢占，完成，死锁};l0= {等待};C= {sch-clocks［x］，switch-clock}，V={t，x，T，o，s}，其中s 为切换时间，t 为当前获得执行权限的线程，o为被抢占线程的个数.

2 AADL 调度模型时间自动机设计

2.1 非可抢占调度策略时间自动机设计

根据AADL 中线程自动机的情况，设计了非可抢占调度策略下周期线程的时间自动机模板(见图2).由图可知，当局部时钟k 达到周期时间P 后，线程从初始状态转移到准备状态，并产生派发信号dispatch［x］!，并且将线程信息赋值给全局变量.sch-info［x］［0］存储线程的最大执行时间Wmax，sch-info［x］［1］存入了线程的优先级F.线程自动机接受调度器的同步信号决定了运行和初始状态的转移.当局部时钟k 超过线程规定的截止时间D 时，自动机进入错误状态，并通过错误通道将错误信号发送给调度器模板.

图2 非可抢占调度策略下周期线程时间自动机模板

根据非可抢占调度策略的调度规则，设计了相应的调度器模板(见图3).由图可知，初始状态为等待状态，调度器Ⅰ和完成是2 种限制状态，在该状态下不发生时间流逝.在状态转移中，分别处理在不同状态下接收到线程派发信号后调度器对新派发线程的处理.调度器维护了一个线程的等待队列ready-q，新派发的线程dispatch［x］首先进入该队列并按照优先级计算策略进行排序，此处T 表示当前派发线程的个数，在非可抢占调度策略下，线程一旦进入运行状态，在执行结束之前是不能进行中断的，并通过completion 函数对ready-q 进行维护.若系统中的任何一个线程超时而进入错误状态，调度器时间自动机通过错误广播通道接收到错误信号后进入死锁状态，自动机停止执行.

图3 非可抢占调度策略下调度器时间自动机模板

在AADL 模型中，处理器组件的属性Thread-Swap-Execution-Time 规定了线程切换的时间开销.为了实现这种转换，扩展了非可抢占调度策略下调度器的模板，设计了带有线程切换时间的非可抢占调度器模板(见图4).模板扩充定义了切换时钟switch-clock 和设置切换时间s，去掉调度器Ⅰ状态的限制属性，增加switch-clock ＜=s 的不变条件，以实现线程状态在时间切换时的模拟，并对该状态的转出条件和通向死锁状态的路径进行了相应调整.

图4 非可抢占调度策略下带有线程切换时间的调度器模板

2.2 可抢占调度策略时间自动机设计

与非可抢占调度策略相比，可抢占调度策略下周期线程的时间自动机模板增加了一个被抢占状态.当运行状态线程的运行权限被更高优先级的线程抢占后，该自动机进入抢占状态，待优先级高的线程执行完毕，被抢占的线程恢复执行，返回运行状态.在该状态下，执行时钟不增长，截止时钟持续增长.线程的抢占加大了恢复调度器模板的复杂程度，相对于非可抢占调度器的模板，状态集合增加了调度状态Ⅱ和抢占状态2 个状态.在运行状态下，当有新的线程派发时，调度器转移到调度器Ⅱ状态，判断新派发线程的优先级.在该时间自动机模板中，引入了被抢占线程栈preempt-stack［z］［2］，记录了被抢占线程的标号和被抢占时间，位于栈顶的元素具有最高的优先级.

在UPPAAL 工具中，时钟参数的初始值为0或为一个比较结果(当前时钟参数与固定整数的差值).基于这一限制，对可抢占调度器模板中被抢占时间的计算方法进行设计.定义指定线程t 的执行时间为Wt，截止时间为Dt，时间自动机中的运行时钟为ct，截止时钟为dt，恢复时的被抢占时间为Pt，已派发线程的优先级高于线程t 个数为n，则有

假设存在3 个线程t1，t2，t3，优先级满足Priority(t1)＜Priority(t2)＜Priority(t3).如图5所示，在点X 处线程t1产生派发，运行时钟ct1和截止时钟dt1都被置为0，此时队列中t1的优先级最高，故被抢占时间Pt1=0;在点Y 处，更高优先级的t2派发，t1需要等待t2线程执行完毕后才能恢复执行，则t1的抢占时间Pt1等于t2的执行时间Wt2与t1已有的抢占时间之和;当更高优先级的线程t3在点H 处被派发时，则t1的抢占时间等于t3的执行时间与t1已有的抢占时间之和.在点O 处，判断条件ct1≥Wt1+Pt1判断了t1除去被抢占时间实际运行的时间是否大于或等于t1的执行时间Wt1，若满足，则t1执行完毕.判断条件dt1≥Dt1判断t1的执行是否超过了规定的截止时间.

图5 线程抢占执行示意图

若计入线程切换的时间，则

式(2)中，由于一次抢占带来2 次线程的切换，故在线程恢复时共进行了2n 次的线程切换.

2.3 可调度性验证语句

UPPAAL 验证器中利用时序逻辑TCTL 可以验证一些基本性质，如线程死锁.对于调度模型的可调度性验证，所使用的部分性质验证语句见表1.

表1 模型可调度性性质验证语句

3 自动化模型转换插件的功能

本文基于AADL 建模工具OSATE 设计开发了自动化模型转换的插件AadlToUpaalL Convert Plug-in，并将其嵌入到OSTATE 工具中，形成了AADL 模型的建模、转换、验证与分析的集成开发环境.自动模型转换插件实现了如下三大功能:①AADL 模型解析.即负责读取建模工具中建立的AADL 模型，按照语义信息与格式规范，解析AADL 模型在转换中所需的基本信息，构建在插件程序中AADL 的对象模型.②模型转换.即根据文本建立的模型转换规则，将读入的AADL 模型信息对应映射为时间自动的基本元素，构建时间自动机的对象模型.③时间自动机模型生成.即解析文件格式，并将得到的时间自动机对象模型转换为模型文件，实现了模型自动构建的功能.由于时间自动机在UPPAAL 工具中以状态图的形式展示，文件中也保存了图形的基本信息，故目标文件生成模块还需要调整模型文件中状态和边的坐标信息.

图6 自动化管焊系统焊枪速度控制模块AADL 模型结构

4 系统测试

4.1 实例测试

本文以自动化管焊设备焊枪速度控制系统为例，建立了系统的AADL 模型，该模型由系统组件(WeldingSystem)、处理器组件(Processor1)、进程组件(Process1)、线程组件(CalThread，Th1，Th2)、设备组件(Sensor1，SpeedActuator)和若干端口、连接组成.其功能是通过一个传感器采集到焊枪枪头电机的转速信息并传递给计算线程，由计算线程处理后产生控制信号传递给控制设备，从而形成一个速度调节反馈的系统.该模型结构如图6所示.

在OSATE 工具中，建立含有3 个周期线程的AADL 系统模型.语法验证通过后，实例化系统得到AAXL 类型的系统模型文件.利用模型转换插件对模型进行自动转换后，在UPPAAL 工具中模拟系统的状态转移，在验证器中利用自动生成的性质查询语句验证系统的时间特性.经测试，系统不发生死锁且Exist ＜＞Processor.MissedDeadline 性质不满足.

4.2 性能分析

本文设计了一组包含20 个线程的测试用例，每个线程的周期和截止时间均为20 ms，执行时间均为1 ms，线程的优先级按照数字序号依次设定为0 ～19.根据Liu 等［13］针对RMS 调度策略提出的使用率限定定理，理论上确定该组任务的所有子集都是可调度的.可调度的任务集合对应的时间自动机性质的验证需要遍历整个状态空间，耗时较长.性质验证计算过程中，UPPAAL 服务进程的CPU 利用率稳定在25%左右，内存消耗随着验证的推进而不断增长，验证时间和内存使用的趋势图分别见图7和图8.

图7 验证耗时随周期线程数变化图

图8 验证内存消耗随周期线程数变化图

5 结语

利用时间自动机形式化验证手段，研究了AADL 模型中调度模型到时间自动机模型的转换方法.设计了非可抢占与可抢占策略下的时间自动机模板以及AADL 模型元素到时间自动机模板的转换法则.利用UPPAAL 与时间自动机模型来验证AADL 所描述系统的可调度性.下一步的研究主要集中于扩展所设计的时间自动机以及模型转换法则，使其支持更多的调度策略以及更复杂的AADL 模型表述.

References)

［1］ Kleppe A G，Warmer J B，Bast W.MDA explained:the model driven architecture:practice and promise［M］.Boston，USA:Addison-Wesley Professional，2003:1-20.

［2］ Peled D A.Software reliability methods ［M］.New York，USA:Springer Science ＆ Business Media，2013:100-125.

［3］ Singhoff F，Legrand J，Nana L，et al.Scheduling and memory requirements analysis with AADL［C］//Proceedings of the 2005 Annual ACM SIGAda International Conference on Ada.Atlanta，GA，USA，2005:1-10.

［4］ Singhoff F，Plantec A，Dissaux P，et al.Investigating the usability of real-time scheduling theory with the Cheddar project［J］.Real-Time Systems，2009，43(3):259-295.

［5］ Gui S，Luo L，Li Y，et al.Formal schedulability analysis and simulation for AADL［C］//ICESS'08 International Conference on Embedded Software and Systems.Chengdu，China，2008:429-435.

［6］ Abdoul T，Champeau J，Dhaussy P T，et al.AADL execution semantics transformation for formal verification［C］//13th IEEE International Conference on Engineering of Complex Computer Systems.Belfast，Northern Ireland，2008:263-268.

［7］ Hu K，Zhang T，Yang Z，et al.Exploring AADL verification tool through model transformation［J］.Journal of Systems Architecture，2015，61(3/4):141-156.

［8］ 符宁，杜承烈，李建良，等.AADL 分级调度模型的分析与验证［J］.计算机研究与发展，2015，52(1):167-176.Fu Ning，Du Chenglie，Li Jianliang，et al.Analysis and verification of AADL hierarchical schedulers［J］.Journal of Computer Research and Development，2015，52(1):167-176.(in Chinese)

［9］ Chkouri M Y，Robert A，Bozga M，et al.Translating AADL into BIP-application to the verification of realtime systems［M］//Models in Software Engineering，Berlin，Germany:Springer，2009:5-19.

［10］ Clarke D，Lee I，Xie H L.VERSA:a tool for the specification and analysis of resource-bound real-time systems，MS-CIS-93-77 ［R］.Philadelphia，PA，USA:Department of Computer and Information Science，University of Pennsylvania，1993.

［11］ Hugues J，Zalila B，Pautet L，et al.From the prototype to the final embedded system using the Ocarina AADL tool suite［J］.ACM Transactions on Embedded Computing Systems (TECS)，2008，7(4):42-1-42-25.

［12］ Johnsen A.Architecture-based verification of dependable embedded systems ［D］.Västerås， Sweden:Mälardalen University，2013.

［13］ Liu C L，Layland J W.Scheduling algorithms for multiprogramming in a hard-real-time environment［J］.Journal of the ACM (JACM)，1973，20(1):46-61.