Page 91 - 《软件学报》2021年第6期
P. 91

陆寅  等:面向 AADL 模型的存储资源约束可调度性分析                                                    1665


         对系统进行形式化建模,然后进行推理分析和仿真运行,进而分析系统的可调度性;除此之外,aadl2sync 工具集
         支持 AADL 模型可调度性的形式化验证,但是 aadl2sync 并不支持 AADL 建模,并且在转换过程中存在缺陷,如
                                                           [9]
         将异步概念转换为同步概念,导致 AADL 模型不能完全转换 ;Brest 大学开发的开源的实时调度计算框架
         Cheddar 工具可支持多种调度策略,支持 AADL 端口延迟、共享资源、消息队列的分析                         [10] ;国内研究者李振松
         等人结合 AADL 中的行为模型附录(behavior annex,简称 BA),根据 AADL 中行为模型的语法语义提出了行为模
         型到 UPPAL 工具的时间自动机模型转换规则,并且证明转换的正确性与有效性,在 UPPAL 工具下对系统的可
         调度性进行仿真验证        [11] .然而这些工具只考虑处理器单一资源下的可调度性分析,而在系统规划阶段,系统的架
         构设计需要综合分析评估多种资源配置下的系统可调度性.
             复杂嵌入式实时系统通常采用抢占式调度策略来保障对关键任务处理的及时响应,抢占会对系统中任务
         的执行时间造成不确定性,从而增加计算成本.例如,抢占可能会导致高速缓存被干扰,被抢占任务的缓存块替
         换出高速缓存,当被抢占任务重新执行时则需要重新加载这些被替换出去的缓存块,这重复加载的时间就称为
         缓存相关抢占延迟(cache related preemption delay,简称 CRPD).在国内,有研究者提出了 CRPD 的计算方法,例如
         UCB-ECB Union 算法,同时,作者也给出了该方法与其他算法之间的比较结果                    [12] .Hai Nam Tran 等人通过建立任
         务的控制流图(control flow  graph,简称 CFG),提出一种抢占任务路径分析的 CRPD 计算方法,为 CFG 中的每一
         个节点定义有用缓存块(useful cache block,简称 UCB)以及抢占缓存块(evicting cache block,简称 ECB),用 UCB-
         Union 计算方法对任务的 CRPD 进行计算         [13] .该方法提供了很好的思路去计算可执行构件动态运行时抢占行为
         所造成的抢占代价.同时,Hai Nam  Tran 提出了 AADL 缓存建模方法,使用 AADL 中的 Subprogram 构件对程序
         控制流图进行建模,然后使用 Ada 语言扩展 Cheddar 工具,使其能够根据程序控制流图对 CRPD 进行计算                          [17] .另
         外,为了保障复杂嵌入式系统任务之间的隔离,减少错误传播和干扰,通常需要采用分区调度策略,实现运行于
         同一计算平台中的不同安全性等级应用之间相互隔离.通过保障各分区任务的实时性,进而提高整个系统的可
         靠性和安全性.然而在架构设计层面,AADL 不能刻画程序执行的具体控制流图,故无法使用 AADL 现有的建模
         与分析方法计算出构件交互的抢占延迟.所以在对 CRPD 进行计算时,为了克服在模型层面上没有具体代码、
         具体实现控制流和数据流信息的问题,本文提出一种基于抢占序列的 CRPD 计算方法,该方法可以不用关心模
         型构件的具体代码实现,能够普适地分析 AADL 调度模型在 CRPD 约束下的可调度性.
             本文面向复杂嵌入式系统,针对系统架构设计的早期阶段,研究在缓存相关抢占延迟约束下 AADL 模型的
         可调度性,通过扩展 AADL 存储资源建模技术,建立包含基本调度元素的分区内架构模型以及符合 ARINC653
         标准的分区系统架构模型          [15] ,研究 AADL 架构模型在缓存相关抢占延迟约束下的可调度性问题,并提出了基于
         抢占序列的 CRPD 计算方法以及 CRPD 约束下的 WCET 计算方法.该计算方法不关心 AADL 线程构件的具体
         代码实现,更适用于软件开发前期 AADL 架构模型实时性分析场景.在嵌入式软件模型设计期,提供缓存抢占延
         迟约束可调度性理论指导,避免在嵌入式软件开发过程中,由于任务之间抢占代价过高而导致系统实时性不达
         标进而造成重复开发的问题.
             本文第 1 节针对 AADL 在缓存资源建模不足的方面进行资源建模能力扩展.第 2 节首先介绍缓存以及缓
         存相关抢占代价的计算方法,结合特定调度策略,分析系统架构中各构件运行行为造成的缓存相关延迟,提出一
         种基于抢占序列评估延迟的计算方法,并制定存储资源约束的任务集可调度性的判断方法和调度策略.第 3 节
         设计一种 AADL 架构可调度性分析工具原型架构,开展缓存约束下的某机载开放式智能信息系统可调度性分
         析案例实验.最后对本文的工作进行总结和展望未来的研究工作.

         1    AADL 缓存资源建模

             AADL 是一种用来设计和分析复杂实时嵌入式系统架构模型和分析非功能属性的建模语言,提供了存储
         资源 Memory 构件对系统存储资源进行建模,并且通过绑定机制刻画软件构件所使用的存储资源属性.AADL
         模型支持层次化存储建模          [13] ,使用 Memory 构件作为 Memory 构件的子组件来描述 Memory 的层次结构,并通过
         软件绑定到 Processor 构件关系来对软硬件视角下的存储资源形成一个映射,将存储器以段为单位进行划分.但
   86   87   88   89   90   91   92   93   94   95   96