体系结构分析与设计语言(Architecture Analysis and Design Language,AADL)[1, 2]由美国汽车工程师协会(Society of Automotive Engineers,SAE)提出,被认为是描述复杂实时嵌入式系统的标准语言,已得到欧美航空航天领域(如Airbus、Boeing、Honeywell、Lockheed Martin、Rockwell Collins)的大力支持. AADL的语言规范详见文献[1, 2].AADL中端到端流(end-to-end flow)能够描述交互信息在系统各部分之间的传输及其时间属性.作为一种半形式化的描述语言,AADL缺少对系统的形式化描述,其不可执行性也决定了其无法直接仿真AADL模型以评估系统特性.
常用的方法是将AADL模型转化为其他形式化模型,再借助这些模型的理论或工具间接分析AADL模型的实时性能[3, 4, 5, 6].但由于缺少对延迟属性的系统性分析与总结,现有的这些方法只考虑了部分时间属性,对关键时间属性的遗漏必然导致分析结果精确度不够;另一方面,当前主要分析最坏情况下的流延迟,而不考虑随机情况下的延迟.而系统中的一些重要的设计,例如事件的发生概率、组件的周期性等,均易对系统的实时性产生不确定的影响,而这些影响往往是系统的时间性能改进的关键.
本文提出一种基于时间自动机的AADL模型中端到端流的延迟分析方法.为保证延迟属性的覆盖率,全面地挖掘与分析AADL核心语言中流延迟的影响因素,建立延迟属性元模型;提出AADL端到端流转化到时间自动机模型的方法,转化过程保证流传输逻辑以及延迟属性语义的正确性;时间自动机模型仿真通过穷举系统状态的变迁过程来表达多样的交互场景,提高对交互场景分析的全面性,并同步获取时间因素的变化过程,提高延迟分析的灵活性.为求简便,下文将AADL中端到端流简称为E2E流.
1 AADL模型实时性分析相关研究当前,对AADL模型实时性分析的研究主要分为两个方向:①较宏观的基于完整AADL模型的时间性能分析；②专门针对E2E流延迟分析.
基于完整模型的性能分析方面,文献[7]研究用工具Topcased形式化验证AADL模型,利用模型转换技术完成AADL-Fiacre-Tina验证链,但AADL与Fiacre模型间的一致性难以保证.文献[8]将AADL模型转换到RTC(Real Time Calculus)模型,根据调度策略及资源约束关系构建抽象组件关系图,再转化到RTC分析硬实时系统的性能.但由于RTC无法基于状态建模,不能表达各事件之间的因果关系,到达曲线也就无法反映流传输的时序信息,导致分析结果粗糙.文献[9]重点研究AADL模型中的模式结构以及线程行为,提供OSATE的插件AADL2Maude实现可执行实时Maude代码的自动生成以便于模型的仿真和性质的验证,但并未考虑传输延迟等时间因素.文献[10]用抽象时间自动机精确描述了AADL模型中的模式变迁语义,工具AADL2TASM实现模型的自动转换并且提出AADL模型的验证框架.文献[11]用CSP(Communicating Sequential Processes)对AADL模型中各种类型组件模型的特征及交互语义做形式化表达,但不考虑时间属性的语义.文献[12]对AADL模型的可靠性和可调度性分析方面的研究作了简单的总结,提到时间自动机是可调度性验证的一个非常重要的形式化模型.文献[13]主要关注AADL模型的可靠性验证.
在专门针对E2E流延迟分析方面,文献[4]经美国国防部倡导,由CMU(Carnegie Mellon University)于2007年做的关于AADL流延迟分析的技术报告.该报告详细解读了延迟属性的语义并给出E2E流延迟的静态分析框架,但此分析框架只对较为典型的组件交互场景进行了分析,例如在周期组件同步交互中要求组件的周期相同,且同时调度.INTRA在文献[4]基础上进一步研究,于2008年发表研究报告[5],报告采用UML MARTE(Modeling and Analysis of Real-Time and Embedded systems)的时间图对AADL的流建模,采用CCSL语言对AADL模型的时间语义做精确描述,但UML MARTE模型不能很好地支持形式化分析与验证.文献[6, 14]详细分析了即时连接与延迟连接这两种数据连接方式的语义,并分别采用MARTE和BIP对其形式化表达,但没有进一步的分析工作.文献[15]用下推自动机PDA定义流的检测模型,用状态转换函数描述流的传输过程,但文献[15]没有分析组件的周期性及组件的调度影响等重要因素.
综上,基于完整模型的分析方法主要在对AADL模型进行语义形式化描述的基础上分析系统的时间性能.这种方法侧重于分析系统的结构与行为,对流的传输逻辑以及延迟属性的关注不够.而专门对E2E流的建模与分析研究虽更细致地研究了属性语义,但这部分研究侧重于对延迟属性语义的理解及手工分析框架的建立,分析效率低,分析场景有限.实时系统中任务的执行时间及组件的交互场景均有随机特性,需要动态灵活的分析方法.再者,为系统的设计模型提供改进的依据与建议是对模型实时评估的重要目的,需要分析并展示各设计决策对实时性的影响.因此,本文研究一种自动化流延迟分析方法,支持完备的延迟属性和多样的交互场景,并且分析过程能支持设计模型的改进.
2 时间自动机时间自动机是有限自动机模型在时间域的一种扩展,它自提出后便一直广泛应用于描述时间系统,其能够对时间语义进行精确的刻画,有助于对体系结构的分析与验证.Alur和Dill在1994年首次提出时间自动机理论[16]并给出时间自动机的定义.
一个时间自动机T可以用一个六元组来表示
3 案例背景文献[17]是由CMU创建并维护的AADL的综合平台,负责发布与更新AADL的权威资料,其中综合化航电系统模型(Integrated System Model)是CMU于2007年建立的比较完整的符合ARINC653规范的模型,主要包括4个子系统,分别为显示管理子系统、显示内容管理子系统、飞行管理子系统以及飞行指引子系统.每个子系统为一个分区,分区之间由网络连接.综合化航电系统模型是嵌入式系统架构的经典案例[18].综合化航电系统模型针对E2E流设计了专门的实现层,本文以飞行管理子系统FlightManager中E2E流的实现方式之一的FlightManager.noPIO为例进行说明.此信息流是飞行管理子系统向显示内容管理子系统请求数据,然后显示内容管理子系统向飞行指引子系统请求并获得相关数据,并最终经过一定处理将数据传给飞行管理子系统的过程.该流涉及显示内容管理子系统、飞行管理子系统和飞行指引子系统,每个子系统由多个子组件实现,子组件之间有大量交互.
为使得流的表示更清晰,处理更方便,本文以飞行管理子系统为中心将各子系统的实现组件进行屏蔽以将流抽象,流示例如图 1所示.图 1中端口组FMTOPCM负责飞行管理子系统与显示内容管理子系统的通信,端口组FMTOFD是飞行管理子系统和飞行指引子系统的通信接口,pageFeed是显示内容管理子系统中负责接收页面显示命令及发送显示页面的接口组.本文将显示内容管理子系统的延迟属性表示为FMTOPCM的属性,将飞行指引子系统对页面请求的处理延迟表示为FMTOFD的属性.
 |
| 图 1 案例E2E示意图Fig. 1 Schematic of E2E of case study |
| 图选项 |
流的描述为:
cmd_request:
FMTOPCM.request→pageFeed.New_Page_Request_ From_PCM→pageFeed.New_Page_Request_To_FD→FMTOFD.request
show_page:
FMTOFD.page→pageFeed.New_Page_Content_From_FD→pageFeed.New_Page_Content_To_PCM→FMTOPCM.page
本文将原信息流进行抽象后,在原模型中流定义的基础上做了扩展:将两条单向流合并为一条往返流,即端口FMTOFD.request接收到请求命令后,传递给飞行指引子系统,飞行指引子系统对请求命令处理后生成页面信息通过FMTOFD.page端口返回.流的所有时间属性:FMTOPCM.request端口的最大发送延迟为5 ms,FMTOPCM.page端口的最大接收延迟为5 ms;周期线程pageFeed的最小执行时间为1 ms,调度周期为50 ms,执行截止时间为50 ms;FMTOFD中页面请求信息的最小处理延迟为4 ms,最大处理延迟为18 ms.
4 E2E流延迟分析方法 4.1 E2E流延迟分析框架时间自动机描述了系统状态与时间变量间的映射关系.系统状态变迁过程伴随着时间变量的累积.通过穷举时间自动机模型的状态变迁序列能够展现组件的所有交互场景,也同步展示时间属性的逐步变化过程.基于此,本文利用时间自动机来分析E2E流延迟,方法如图 2所示.
本方法的步骤如下:
1) 总结完备的流延迟属性,建立E2E流延迟属性的元模型,为面向延迟分析的E2E流的时间自动机建模提供指导.
2) 建立E2E流的时间自动机模型.为了保证延迟分析结果的可靠性,正确表达流的传输逻辑及延迟属性语义.正确无二义的时间自动机模型是延迟分析的前提与基础.
3) 运用工具对时间自动机模型进行仿真与分析.仿真中观察时间属性的变化,展现交互组件间信息的传递过程,验证流的传输逻辑,包括有无死锁等结构逻辑和流的语义逻辑,检验AADL模型中各延迟属性参数设计的合理性.
 |
| 图 2 E2E流延迟分析框架Fig. 2 E2E flow latency analysis framework |
| 图选项 |
4.2 延迟影响因素分析E2E流表示一系列组件端口的连接逻辑,延迟分析是对AADL模型中由E2E流关联的对流延迟有贡献的属性值的综合分析与度量.流延迟由组件自身的执行时间和组件间的交互延迟组成.组件间的交互延迟包括组件内信息的收发时间,由信息排队等引起的延迟以及由传输协议引起的传输延迟.表 1为AADL的组件和流的正则语法定义,可知组件的组成部分包括特征、流以及相关属性,端口、端口组和参数构成流的传输结点.据AADL标准,端口可分为数据端口,事件端口和事件数据端口3类,端口组是端口的组合表示.参数表示调用子程序时的输入/输出值,子程序是组件可调用的可执行源代码.因此组件的执行延迟属性、子程序调用延迟以及端口间的交互延迟属性构成必要且完备的延迟属性集.
表 1 AADL规范组件及流的语法定义Table 1 Component and flow syntax in AADL specification
| 组件定义 | component_type::=component_category defining_component_type_identifier[features ({feature}+|none_statement)] [flows({flow_spec}+|none_statement)][properties({component_type_property_association}+ |none_statement)]{annex_subclause}*end defining_component_type_identifier; component_category::=software_category|execution_platform_category|composite_category; software_category::=data|subprogram|thread|thread group|process; execution_platform_category::=memory|processor|bus|device; composite_category::=system |
| 流定义 | flow_spec::=flow_source_spec|flow_sink_spec|flow_path_spec; flow_spec_refinement::=flow_source_spec_refinement|flow_sink_spec_refinement|flow_path_spec_refinement; flow_source_spec::=defining_flow_identifier:flow source flow_feature_identifier[{{property_association}+}]; flow_sink_spec::=defining_flow_identifier:flow sink flow_feature_identifier[{{property_association}+}]; flow_path_spec::=defining_flow_identifier: flow path source_flow_feature_identifier->sink_flow_feature_identifier[{{property_association}+}]; flow_source_spec_refinement::=defining_flow_identifier:refined to flow source {{property_association}+}; flow_sink_spec_refinement::=defining_flow_identifier:refined to flow sink {{property_association}+}; flow_path_spec_refinement::=defining_flow_identifier:refined to flow path {{property_association}+}; flow_feature_identifier::=port_identifier|parameter_identifier|port_group_identifier|port_group_identifier.port_identifier |
表选项
据AADL标准,子程序访问的时间约束包括远程调用的截止期(Compute_Deadline)和最大执行时间(Compute_Execution_Time),均是对调用子程 序的线程约束,故本文不针对子程序调用做专 门的研究,而将相关延迟纳入线程的延迟属性考虑范围.端口组是端口的逻辑组合,本文不做赘述.另外,虽然AADL允许用户扩展属性集,本文只对AADL标准中核心属性集作分析,此方法同样适用于扩展的属性.
通过对AADL规范中组件与端口及参数依赖关系的分析和相关属性的研究,总结提出面向延迟分析的延迟属性元模型如图 3所示,为面向延迟分析的时间自动机建模提供准备与指导.系统中传输流信息的基本组件类型包括线程、设备和处理器.端口间连接类型包括数据连接、事件连接和事件数据连接.
 |
| 图 3 E2E流延迟属性元模型Fig. 3 E2E flow latency-contribution attribute metamode |
| 图选项 |
按端口类型分析延迟属性的语义为:
1) 数据端口(data port).
如图 3所示,数据连接可能发生在两线程之间或是处理器与线程、设备与线程之间.数据端口间有延迟连接和即时连接两种方式.当两线程间是即时数据连接时,源线程执行完毕之时即是数据传输开始之时.AADL标准要求即时连接的两个线程必须同时调度,但目标线程必须在收到传输数据后方可执行.当两线程的端口间是延迟连接时,数据传输自源线程运行的截止时刻(deadline)开始,源线程与目标线程不必同时调度,目标线程总是利用源线程最新调度时产生的数据.当处理器或设备的端口与线程端口间是数据连接时,目标线程被调度时,就是传输的开始时刻.组件类型及调度属性、周期线程间的同步/异步、数值传输的开始时刻与完成时间等因素形成多样的组件交互场景,都是数据连接延迟的不确定性因素,正确地表达这些因素是分析的基础.
2) 事件端口(event port)和数据事件端口(event data port).
组件间的异步事件可通过事件端口交互,数据事件端口用于状态数据传输.这两种机制都需排队实现,将事件或状态数据按序暂存起来,再按某种方式(默认FIFO)获取.AADL中有AllItem、OneItem和MultipleItems 3种出队协议.AllItem时,Queue_Size规模的事件/数据事件全部出列.One-Item时,某一事件/数据事件出列即可.MultipleItems时,多个事件/数据事件同时可用.属性Overflow_Handling_Protocol规定当事件的到达间隔小于线程的处理周期时系统应采取的行为,可以选择忽略事件,排队等待下个调度周期或者视作错误处理.Queue_Processing_Protocol规范了事件及状态数据的排队处理顺序如FIFO.
4.3 E2E流的时间自动机建模方法 4.3.1 时间自动机表达能力分析1) 数据连接的表达.
即时连接与延迟连接这两种数据连接方式对流延迟影响的差异性主要表现为源端发送数据的时刻以及目标端接收数据的时刻不同.据时间自动机的定义[16],位置可表达数据发送/接收的开始/终止状态,位置不变式可表达处于该状态的时间上限要求,映射到流延迟属性可以是线程的最大处理时间maxExecTime即max{Compute_Execution_Time,Recover_Execution_Time},线程执行的截止期deadline,即{deadline,period}或连接延迟的上限maxLatency即max{Latency,Expected_Latency,Actual_Latency}.转移时钟守护条件可以用于约束下限{minExecTime,minLatency},其中minExecTime=min{Compute_Execution_Time,Recover_Execution_Time},minLatency=min{Latency,Expected_Latency,Actual_Latency}.
时间自动机的执行语义可表达为
即时连接:对于状态(BSend,ν(maxExec-Time,deadline,maxLatency)),若 δ≥0∧ν+δ∈I(BSend)∧δ∈φ(minExecTime,minLatency),则(BSend,ν(maxExecTime,deadline,maxLatency))→(ASend,ν[λ:=0]).
延迟连接:对于状态(BSend,ν(maxExec-Time)),若 δ≥0∧ν+δ∈I(BSend)∧δ∈φ(deadline),则(BSend,ν(maxExecTime)) δ (ASend,ν[λ:=0]).
其中:BSend与ASend分别为数据发送前与发送后的位置;I为位置与其不变式之间的映射关系;ν∈I为位置的时钟约束;ν[λ:=0]表示将转到此位置时将时钟重置，即时连接中数据发送发生在源端线程执行完毕时,时钟使能条件时钟值不小于minExecTime或minLatency,延迟连接中的源端组件执行截止期时刻开始数据的发送,因此时钟使能条件是时钟值等于deadline.
2) 事件连接与数据事件连接的表达.
时间自动机的建模仿真工具,如UPPAAL4.0中允许用户自定义函数来扩充时间自动机模型,这些函数可以访问和修改所有的状态变量.通过设置数据结构如数组来暂存到达的事件/数据,所设置的数组变量类型应能够标识数据元素类型.用函数实现对Dequeue_Protocol,Overflow_Han-dling_Protocol以及Queue_Processing_Protocol模拟以及排队延迟的计算.
4.3.2 E2E流的时间自动机建模方法将时间自动机模型描述为多个并行时间自动机的积系统,是模块化思想在时间自动机模型中的运用,可以极大地降低模型构造的复杂度,同时也提高本文方法的实用性.本文称单个时间自动机为原子模板.由时间自动机的定义,时间自动机模型可分为位置集,位置不变式以及转移条件.因此本文建模过程包括4个步骤:设置原子模板集合,设置位置集合,设置位置不变式以及转移条件.状态空间爆炸问题几乎是所有实时模型检测方法必须要面对的,也是影响模型检测方法实用性的最大障碍.为了尽量避免此问题,应尽可能减少原子模板数目和模板中的位置数目.因此,本文分析端到端的抽象层次,灵活设置原子模板的方法,以保证较少的原子模板数目;根据流传输逻辑,将所有可能的位置分类设置来减少模板中位置的数目.当需要分析大型复杂系统底层组件的延迟属性时,本文采用分层嵌套的方式,即将底层组件的流延迟属性计算后封装为高层组件的延迟属性.这是模块化思想在流延迟分析中的运用,不仅简化了时间自动机模型的设计,而且便于定位设计模型中的不足以求改进.E2E流向时间自动机模型的具体转化流程如图 4所示.
 |
| 图 4 E2E的时间自动机建模流程Fig. 4 Modeling process of E2E timed automata |
| 图选项 |
建模过程的具体步骤如下:
1) 设置原子模板.首先分析流的传输逻辑,决定时间自动机模型的抽象层次.流表达信息在结点间的传输过程,流的传输逻辑造成传输结点有限的状态改变.以流传输结点为模板,当传输结点数目较多时,将流抽象表示.本文建议原子模板数目不超过7个.常见的传输结点有子系统,组件以及端口3种.对于周期性结点,本文设置周期调度器模板,见图 5.以案例模型为例,由于组件及组件间的交互繁多,本文将流抽象为子系统之间的交互,将原子模板个数设为4个(包括周期调度器).
 |
| 图 5 周期调度器模板Fig. 5 Period component’s dispatcher template |
| 图选项 |
2) 设置模板位置.为了保证流的传输逻辑,跟踪信息的转移,将所有对信息有处理作用的过程映射为时间自动机的候选位置.接着,为保证较少的位置集合,按信息的处理逻辑将候选位置集分类.流的传输过程包括对信息的发送、处理、接收以及通信结点之间的传输.有时需要设置无实际含义的辅助位置,因此位置集合L={信息接收位置,信息发送位置,信息处理位置,信息传输位置,辅助位置}.
时间自动机中只有在位置上才有时间消耗,位置间的转移是瞬时的,信息接收及接收的延迟发生在收到发送方的信号之后,因此信息接收位置位于接收信号所在转移的箭头所指位置.同理,信息发送位置位于信息发送信号所在转移的箭尾位置,信息处理位置设于信息接收位置与信息发送位置之间.
传输过程中,由于传输距离、传输协议、传输介质性能等因素引起传输延迟时,需设置信息传输位置,本文将信息传输位置设在信息发送方.
以案例模型为例,本文设置的位置主要包括infoAccept、infoProcess、cmdAccept、cmdProcess等,分别表示内容信息的接受,信息内容的处理,命令的接收及处理等,此外还有一些辅助位置如wait、idle等.含有语义信息的位置命名方式将有助于对于模型逻辑的审查.
3) 设置位置不变式.位置不变式I(ν)表示位置ν恒满足的时间约束.位置不变式设置不当极易引起时间自动机模型的死锁.当流的传输结点同时有最大执行时限和执行截止期要求时,本文设置位置不变式为c≤maxExecTime,这是因为maxExecTime可以对应到结点的某个状态,而deadline约束整个结点的执行时间,maxExecTime比deadline有更强的约束能力.交互的结点可能位于同一个处理器内或分布于多个处理器间,因此信息可能通过数据总线或者网络传输,当需要分析底层组件的延迟属性,且端到端流模型有介质传输速度以及传输内容规模属性时,可以计算得到传输延迟,具体方法可参考文献[4].本文对延迟属性相关的结点层次不做要求,只要属性值可定量表示即可.不失一般性地设时钟为c,则位置不变式设置过程如下:
① While当前位置∈{信息接收位置,信息发送位置,信息处理位置}do.
② if 有最大计算时限要求then c≤maxExecTime.
③ else if位置有截止期属性then c≤deadline.
④ if当前位置is信息传输位置then
c≤maxLatency.
此处的maxExecTime、deadline、maxLatency的定义同第4.3.1节.
4) 设置转移条件.转移条件是原子模板内位置间的转移约束,也是各原子模板之间同步通信的重要方式.转移条件集合包括守护条件集合A、同步信息集合B和更新信息U,其中守护条件集合A表示转移发生的前提条件,通常是时钟范围以及共享全局变量的要求.同步信息集合B可用来实现原子模板间的通信,UPPAAL中用通道实现同步通信,全局共享变量可实现异步通信.更新信息U通常包括时钟C的重置与共享变量值var的更新.
转移条件的设置过程如下:
① if连接方式∈{即时数据连接,事件连接,数据事件连接}.
② then {(loc≥minExecTime)&& (loc≤maxExecTime)}∈A.
③ else if连接方式is延迟数据连接then{loc= =deadline}∈A.
④ 设置表征调度状态的全局变量active.
⑤ 设置传输通道,包括发送通道与接收通道.
⑥ While C={流传输总延迟时钟sysTime,位置时钟loc,模板上延迟时钟dur}非空do.
⑦ 取φ∈C.
⑧ C=C-{φ}.
⑨ if φ需要重置.
⑩ 重置φ.
B11 更新全局共享变量var.
根据第4.2节的分析,将即时数据连接方式、事件连接与数据事件连接归为一类处理,而对延迟数据连接方式单独考虑.布尔变量active用于表达周期组件是否可调度.为了描述流的传输逻辑,通道连接的原子模板表示通信的组件,通道的名称应有实际含义表达流的语义.
表 2列出了建模过程中部分延迟属性与AADLAS5506标准的对应关系.
表 2 部分E2E流延迟属性在时间自动机Table 2 Part E2E flow latency-contribution attributes in timed automata
| 延迟属性 | 所属组件 | 时间自动机元素 | 在时间自动机中表示 |
| dispatch_protocol | 处理器,设备,线程 | 若组件为周期调度, 构造周期调度器模板 | 由调度策略决定表示形式 |
| period | 线程,设备,处理器,系统 | 位置不变式/转移守护条件 | 位置不变式:loc≤period 转移守护条件:loc==period |
| deadline | 线程,设备,处理器,系统 | 位置不变式/转移守护条件 | dur≤deadline 或dur |
| compute_execution_time | 线程,设备 | 位置不变式/转移守护条件 | 无deadline属性: 位置不变式:loc≤maxExecTime 有deadline属性: 转移守护条件:loc≥minExecTime (loc≤deadline)&&(loc≥minExecTime) |
表选项
5 案例分析本节通过对时间自动机模型的仿真来说明文中方法对端到端流模型的表达能力以及对流延迟的分析能力.首先在第4节的指导下对背景案例模型中的端到端流建立时间自动机模型,之后运用时间自动机模型的仿真与验证工具UPPAAL对该模型进行仿真分析.多次仿真过程模拟多样的流传输场景,每次仿真过程中的消息序列图以直观的方式展示流的传输逻辑;时间自动机模型的时间参数随状态组合的变迁而逐步变化,展示便捷的时间分析能力.为了验证对流延迟属性的延迟语义表达的正确性,本文首先手工分析得出流的最大/最小延迟,然后将其在UPPAAL工具上验证,若验证结果一致,即工具自动仿真结果与手工分析结果吻合,说明本文正确地表达了流延迟属性语义.为进一步说明本文方法的分析能力,第5.3节给出与OSATE的分析能力对比表.最后,第5.4节分析方法的实用性.
5.1 时间自动机建模由第3节的描述可知抽象后的案例流逻辑简单,传输结点少,包括端口组FMTOPCM、线程pageFeed和端口组FMTOFD.将传输结点设置为原子模板,即端口组FMTOPCM和FMTOFD、线程pageFeed.另外由于线程pageFeed的周期性,设置线程周期调度器模板timer.按照第4.3.2节的步骤,依次设置模板位置,位置不变式以及转移条件.
时间自动机模型如图 5~图 8所示.其中图 5为周期调度器模板.图 6中sysTime记录流传输的总延迟,loc记录每个位置上的时间消耗,dur记录单个时间自动机模板的执行时间,布尔变量active用于标志pageFeed是否在可通信状态.
 |
| 图 6 FMTOPCM端口组时间自动机模型Fig. 6 Timed automata of FMTOPCM port group |
| 图选项 |
 |
| 图 7 pageFeed端口组的时间自动机模型Fig. 7 Timed automata of pageFeed port group |
| 图选项 |
 |
| 图 8 FMTOFD端口组时间自动机模型Fig. 8 Timed automata of FMTOFD port group |
| 图选项 |
5.2 模型仿真与验证时间自动机模型的状态变迁包括位置变迁与时钟变化,其中位置变迁轨迹表达流的传输逻辑,时钟变化为延迟的计算过程.仿真时间自动机模型通过穷举时间自动机模型的状态变迁序列,能够展现最坏情况流延迟、最好情况流延迟以及随机流延迟时多样的组件交互场景.状态变迁过程中伴随着时间变量的累加,便于分析多样交互场景下的时间因素变化.
本节通过工具UPPAAL仿真时间自动机模型的过程数据来说明本文方法的描述能力和分析能力.
5.2.1 模型仿真本文用通道描述消息的传输,描述交互的组件双方以及消息内容,UPPAAL对时间自动机模型仿真过程中产生的仿真轨迹图以及消息传输序列图都可以直观地表示各原子模板间的信息交互,其中消息传输序列如图 9所示,其中图 9(a)与图 9(b)分别为两个不同交互场景下的消息序列图.图 9(a)中周期调度器Timer首先发dispatch信号给pageFeed,使之处于ready状态.流的传输开始,此时FMTOPCM组件处于待发送态cmdSend,向pageFeed发送信号fromPCM后处于辅助态mediate.pageFeed由ready态转为接收态cmdAccept,接收完毕后进入信息处理态cmdProcess,处理完毕后向FMTOFD发送信息toFD,发送完毕处于idle态.FMTOFD由idle态转为cmdProcess态,处理完毕后处于cmdSend态,但由于此时pageFeed处于不可通信状态,FMTOFD必须等待Timer发送pageFeed可通讯信号,待接收到dispatch信号后发送fromFD给pageFeed,使其从ready态转为infoAccept态,之后进入infoProcess态,处理完毕后发送toPCM给FMTOPCM,FMTOPCM从mediate态转为infoAccept态,流的一个传输周期结束,与AADL模型流的传输逻辑相同,各组件的执行时间以及组件间信息的传输延时,各组件等待pageFeed的延迟都是造成本案例流延迟不确定的原因.图 9(b)显示了当流传输开始时pageFeed处于不可调度态,此时FMTOPCM必须处于wait态等待,只有接收到Timer发出的dispatch信号后才能转为idle态开始流的传输,分析过程同上.由此可见,时间自动机模型的仿真过程能够表达所有可能的原子模板间的交互场景,而不必单独为每种不同的交互场景分别建模.
 |
| 图 9 交互消息序列示意图Fig. 9 Schematic of interactive message sequence |
| 图选项 |
时间自动机状态变迁过程伴随着时间的变化,也正是由于时间因素的随机性才造成了组件间多样的交互场景.在对时间自动机模型仿真的过程中可以同步观察时间变量的变化.与图 9(a)对应的时间与状态变迁关系见表 3.一组交互场景的状态组合序列为一次流传输过程,由表 3可以观察到各原子模型的位置组合变迁的过程中所有时间参数的逐步变化.本例中sysTime用于统计整个流的传输延迟,各模板的loc时钟用于记录并控制在每个位置的时延,而各模板的dur时钟用于记录并控制各原子模板的执行延迟.用户在使用本方法时,可以根据需要灵活设置时间变量.观察各状态组合及时间参数的变化过程,便于验证模型中时间参数的设计,如表中变迁关系(idle,ready,wait,idle)→(cmdSend,ready,wait,idle)是由于FMTOPCM的request端口发送消息引起,最大的发送延迟为5 ms,故各时间参数的范围为[0, 5].(mediate,cmdAccept,wait,idle)到(mediate,cmdProcess,wait,idle)的变迁由pageFeed处理消息引起,最小处理延迟为1 ms,依此类推,得到FMTOPCM.sysTime的范围为[51, 56],表示此组交互场景下的最小延迟为51 ms,最大延迟为56 ms.若得到的延迟范围不符合用户期望,则通过回溯状态与时间的对应关系定位设计的不合理之处,进行改进.对比所有交互场景组合下的延迟范围,得到端到端流模型的最大/最小延迟.
表 3 时间随状态变化过程Table 3 State transition process with time change
ms
| 状态组合 | FMTOPCM | pageFeed | Timer | FMTOFD | ||
| sysTime | loc | loc | dur | dur | loc | |
| (idle,ready,wait,idle) | 0 | 0 | 0 | 0 | 0 | 0 |
| (cmdSend,ready,wait,idle) | [0, 5] | [0, 5] | [0, 5] | [0, 5] | [0, 5] | [0, 5] |
| (mediate,cmdAccept,wait,idle) | [0, 5] | [0, 5] | 0 | 0 | [0, 5] | [0, 5] |
| (mediate,cmdProcess,wait,idle) | [0, 6] | [0, 6] | [0, 1] | [0, 1] | [0, 6] | [0, 6] |
| (mediate,idle,wait,cmdProcess) | [1, 24] | [1, 24] | [1, 19] | [1, 19] | [1, 24] | [0, 18] |
| (mediate,idle,wait,cmdSend) | [5, 24] | [5, 24] | [5, 19] | [5, 19] | [5, 24] | 0 |
| (mediate,idle,wait,wait) | [5, 50] | [5, 50] | [5, 50] | [5, 50] | [5, 50] | [0, 45] |
| (mediate,ready,wait,cmdSend) | 50 | 50 | [45, 50] | [45, 50] | 0 | [26, 45] |
| (mediate,infoAccept,wait,idle) | 50 | 50 | 0 | 0 | 0 | [26, 45] |
| (mediate,infoProcess,wait,idle) | [50, 51] | [50, 51] | [0, 1] | [0, 1] | [0, 1] | [26, 46] |
| (infoAccept,idle,wait,idle) | [51, 56] | [0, 5] | [1, 6] | [1, 6] | [1, 6] | [27, 51] |
| (end,idle,wait,idle) | [51, 56] | [0, 5] | [1, 6] | [1, 6] | [1, 6] | [27, 51] |
表选项
5.2.2 语义一致性验证1) 最大/最小延迟的手工分析.
由运行环境、任务的到达模式等多种不确定因素所致,实际系统的单次运行时间往往难以精确预测,常用最好情况延迟与最坏情况延迟来预测系统的运行时间范围,保证系统基本的实时性需求.
本节用手工方法来分析示例流的最大/最小延迟.首先需要分析流的最大及最小延迟对应的交互场景.本例中流传输延迟不确定的原因在于FMTOPCM发送/接收消息的时间以及FMTOFD中页面请求信息的处理时间不确定,造成等待线程pageFeed调度周期的时间不确定.因此,当端口组FMTOPCM和FMTOFD与pageFeed的交互延迟之和最小且pageFeed的执行时间最小时,流的传输延迟最小.同理,当端口组FMTOPCM和FMTOFD与pageFeed的交互延迟之和最大且pageFeed的执行时间最大时,流的传输延迟最大.但是端口组FMTOPCM和FMTOFD与pageFeed的交互延迟的最大/最小之和不是两个端口组中相关延迟的最大/最小值的简单相加,两个端口组只能与不同调度周期中的pageFeed交互,必须合理设置pageFeed调度的开始时间.
最小延迟分析如图 10所示,pageFeed从0时刻开始调度,当FMTOPCM发送fromPCM信号给pageFeed,pageFeed已处于ready状态,FMTOPCM的最小发送延迟为0.pageFeed的最小计算时间为1 ms,其采用即时发送的方式将信息传给FMTOFD,故pageFeed对信息的发送耗时1 ms(见图 10(a)).FMTOFD的最小信息处理延迟为4 ms(见图 10(b)),FMTOFD将返还的信息传输给pageFeed时,须等待pageFeed的下次调度,距离上次调度共需耗时50 ms(见图 10(c)).当pageFeed处于被调度状态时,接收返还的页面信息耗时1 ms(见图 10(d)),FMTOPCM耗时0.故此E2E流的最小传输延迟为50 ms+1 ms=51 ms.
 |
| 图 10 最小延迟分析Fig. 10 Least-latency analysis |
| 图选项 |
最大延迟分析如图 11所示,最大延迟为50 ms+50 ms+5 ms=105 ms.
由分析过程可以看出,针对每种流延迟情况需要分析不同的交互场景,本例仅对最大/最小流延迟做分析,笔者花费时间近4 h.而且本例中手工分析无法穷尽所有可能的pageFeed调度开始时间,因而无法对所有延迟情景做分析.
 |
| 图 11 最大延迟分析Fig. 11 Worst-latency analysis |
| 图选项 |
2) UPPAAL验证.
将手工分析的最大/最小延迟结果表示为UPPAAL可验证的TCTL(Timed Computation Tree Logic)语言,待验证的内容、TCTL表达式及验证结果如表 4所示.表 4中首先对时间自动机模型是否存在死锁做验证,验证结果为“满足”.通常,时间自动机模型存在死锁状态说明模型中存在不恰当的位置不变式设置或原子模板间的同步机制造成流传输逻辑的错误,所以通常将死锁状态的检查作为模型评估的第1步.表中第2条与第3条从正反两个方面对流的最大/最小延迟验证.第2条说明UPPAAL仿真得到的流的传输总延迟总是介于51 ms与105 ms之间,与第5.2.2节的手工分析结果一致. 第3条则说明UPPAAL仿真时间自动机模型时不存在传输总延迟小于51 ms或大于105 ms的流传输场景,与上文手工分析结果一致.此结果可证明时间自动机模型的正确性,包括正确的流传输逻辑并和正确的流延迟属性语义. 表 4 最大/最小延迟在UPPAAL中的验证Table 4 Verification of worst-latency and least-latency in UPPAAL
| 序号 | 系统属性说明 | 时序逻辑表达式 | 验证结果 |
| 1 | 无死锁状态 | A[ ]not deadlock | 满足 |
| 2 | 传输总延迟介于51 ms与105 ms之间 | A[ ](FMTOPCM.end imply(FMTOPCM.sysTime≥ 51and FMTOPCM.sysTime≤105)) | 满足 |
| 3 | 存在总延迟小于51 ms或大于105 ms的情况 | E<>(FMTOPCM.end and(FMTOPCM.sysTime< 51or FMTOPCM.sysTime>105)) | 不满足 |
表选项
5.3 本文方法与OSATE流延迟分析能力的对比OSATE是基于eclipse开发的开源工具,其E2E流延迟分析插件是CMU SEI以文献[4]为理论基础而开发的,在AADL建模与分析领域得到广泛认可.通过对OSATE的运用得出本文方法与OSATE流延迟分析插件的对比如表 5所示.
表 5 本文方法与OSATE流滞分析插件对比分析Table 5 Comparison between our proposed method and OSATE flow latency analysis plug-in
方法 | 最坏情况 分析 | 最好情况 分析 | 随机情况 分析 | 底层组件 属性覆盖 | 时间变量 过程跟踪 |
| OSATE | ● | ─ | ─ | ─ | ─ |
| 本文方法 | ● | ● | ● | ● | ● |
| 注： “●”—该行对应的方法具备该列对应的分析能力；“─”—该行对应的方法不具备该列提出的分析能力. | |||||
表选项
由表 5分析可得如下结论:
1) 目前OSATE只分析了最坏情况下的流延迟,对于最好情况以及由于非同步组件的通信等不确定因素造成的随机情况下的流延迟没有做分析;而本文的时间自动机模型描述了流的传输逻辑以及流的传输延迟语义,实时自动机模型的仿真从本质而言是对符号化状态的枚举来遍历系统的状态空间,因此在仿真过程中仿真所有可能的交互场景包括最坏情况、最好情况以及随机情况.
2) OSATE仅以excel文本报告的形式给出最坏情况流延迟分析的最终结果,分析的中间过程不可见;而本文在对时间自动机的仿真过程中以直观的方式展示时间变量的逐步变化过程,方便对时间变量作回溯分析,这对系统模型的设计改进有重要意义.
3) OSATE的流延迟分析是基于直接子组件的时间属性声明实现的,这种方式便于分析的进行,但流在底层组件的传输延迟是系统的实时性能分析不可或缺的一部分;本文采用嵌套的分析方法,将底层组件的流延迟封装为上层组件流延迟的一个属性,因此延迟属性可以是直接子组件的时间属性或者底层组件的延迟属性,有更高的灵活性.
5.4 实用性分析用时间自动机模型仿真的方法评估大型系统模型的一个关键挑战在于状态空间爆炸问题.针对此问题,本方法的第1步要求灵活设置建模层次以控制原子模板数目,而且由于本文方法按传输逻辑对流位置的等价分类处理使得每个原子模板的位置数目少于7个,包括信息接收位置、信息处理位置、信息发送位置、信息传输位置以及可能存在的辅助位置.当对复杂的流进行延迟分析且需要分析底层组件的时间属性时,本文引入模块化思想,以嵌套的方式建模,将底层流延迟分析结果作为上层流延迟属性.这样不仅简化了时间自动机模型的设计,而且模块化层次建模便于定位模型设计的问题,检验模型设计.因此即使对于大规模的复杂流,本文方法也能够保证所建立的时间自动机模型的简单性,避免状态空间爆炸问题.本文以飞行管理子系统为核心,将其他两个系统抽象,并将相关时间属性表示为示例流中端口组的属性,这样以较高的层次将时间自动机模板数目控制为4个.对综合化航电系统中贯穿4个子系统完整的端到端流进行建模,选择子系统为建模层次,原子模板数目为5(其中1个模板为分区调度器模板),平均位置数目为5,由于时间自动机模型较为简单,此处没有罗列.
6 结 论为支持嵌入式系统的实时性评估,本文提出一种基于时间自动机的AADL端到端流延迟的分析方法.
1) 提出面向流延迟分析的延迟属性元模型,保证本文方法涵盖必要且完备的延迟属性集.
2) 给出面向延迟分析的E2E流的时间自动机建模方法,简单、正确地表达流传输逻辑以及延迟属性语义.通过仿真时间自动机模型能够实现流延迟的自动分析.
3) 通过案例验证方法的表达能力及分析能力.当分析结果违背系统的延迟需求时,时间自动机的状态组合序列以及消息传输轨迹图能够为设计模型的审查与改进提供依据和建议.
在未来的工作中,将在以下两个方面继续深入研究:
1) 在保证能精确获得各组件执行所有任务的时间的前提下,为分布式实时系统找到一个可调度的方案仍然是NP完全问题,这不仅要考虑到所有任务的调度,还有考虑到网络信息的传输等[19].而各组件的调度是端到端流延迟分析的基础.本文假设各组件均可调度,后续将深入研究系统的可调度性对端到端流延迟的影响.
2) 本文假设交互组件依赖于同一时钟频率,而不同时钟频率的组件交互可能会导致组件通信时伴有时钟飘移现象,这是硬实时系统中必须要考虑的一个重要因素,也是本文下一步要解决的问题.
致谢 在此,我们向对本文的工作给予支持和建议的同行,特别对北京航空航天大学软件工程研究所吴际副教授和蒋竞老师表示忠心感谢.
参考文献
| [1] | SAE AS5506 Architecture analysis and design language (AADL)[S].Los Angeles,California:SAE International,2004. |
| [2] | Feiler P H, Gluch D P,Hudak J J.The architecture analysis & design language (AADL):An introduction,CMU/SEI-2006-TN-011[R].Pittsburgh,PA:Software Engineering Institute,2006. |
| Click to display the text | |
| [3] | Berthomieu B, Bodeveix J P,Dal Zilio S,et al.Formal verification of AADL models with Fiacre and Tina[C]//Proceedings of ERTSS 2010-Embedded Real-Time Software and Systems,2010:1-9. |
| Click to display the text | |
| [4] | Feiler P, Hansson F J.Flow latency analysis with the architecture analysis and design language (AADL),CMU/SEI-2007-TN-010[R].Pittsburgh,PA:Software Engineering Institute, 2007. |
| Click to display the text | |
| [5] | Lee S Y, Mallet F,De Simone R.Dealing with AADL end-to-end flow latency with UML MARTE[C]//Proceedings of 13th IEEE International Conference on Engineering of Complex Computer Systems,ICECCS.Piscataway,NJ:IEEE Press,2008:228-233. |
| Click to display the text | |
| [6] | André C, Mallet F,De Simone R.Modeling of immediate vs.delayed data communications:From AADL to UML MARTE[C]//ECSI Forum on specification & Design Language(FDL).Belmont:ECSI,2007:249-254. |
| Click to display the text | |
| [7] | Berthomieu B, Bodeveix J P,Chaudet C,et al.Formal verification of AADL specifications in the topcased environment[C]//30th IFIP WG 6.1 International Conference.Berlin:Springer,2010:47-62. |
| Click to display the text | |
| [8] | Sokolsky O, Chernoguzov A.Performance analysis of AADL models using real-time calculus[C]//Proceedings of the 15th Monterey Conference on Foundations of Computer Software:Future Trends and Techniques for Development.Berlin:Springer,2010:227-249. |
| Click to display the text | |
| [9] | Ölveczky P C, Boronat A,Meseguer J.Formal semantics and analysis of behavioral AADL models in real-time Maude[C]//Proceedings of FMOODS/FORTE.Berlin:Springer,2010:47-62. |
| Click to display the text | |
| [10] | Yang Z B, Hu K,Ma D F,et al.Formal semantics and verification of AADL modes in timed abstract state machine[C]//Proceedings of the 2010 IEEE Conference on Progress in Informatics and Computing(PIC).Piscataway,NJ:IEEE Press,2010:1098-1103. |
| Click to display the text | |
| [11] | Yang C X, Dong Y W,Zhang F.et al.Formal semantics of AADL models with machine-readable CSP[C]//Proceedings of 11th IEEE/ACIS International Conference on Computer and Information Science (ICIS).Piscataway,NJ:IEEE Press,2012:565-571. |
| Click to display the text | |
| [12] | Liu W, Liu S Y.Research on the formalization of AADL model[C]//Proceedings of 2013 International Conference on Computational and Information Sciences.Piscataway,NJ:IEEE Press,2013:72-75. |
| Click to display the text | |
| [13] | Ling D Y, Wang S H,Liu B,et al.Reliability evaluation based on the AADL architecture model[J].Journal of Networks,2014,9(10):2721-2727. |
| Click to display the text | |
| [14] | Pi L, Bodeveix J P,Filali M.Reliable software technologies-Ada-europe[M].Berlin:Springer,2009:192-206. |
| [15] | Zhu Y F, Dong Y W,Ma C Y,et al.A methodology of model-based testing for AADL flow latency in CPS[C]//Proceedings of 5th International Conference on Secure Software Integration & Reliability Improvement Companion(SSIRI-C).Piscataway,NJ:IEEE Press,2011:99-105. |
| Click to display the text | |
| [16] | Alur R A, Dill D L.A theory of timed automata[J].Theoretical Computer Science,1999,126(2):183-235. |
| Click to display the text | |
| [17] | AADL website[EB/OL].[2014-10-09].http://www.aadl.info/aadl/testsite/examplemodel.html. |
| [18] | Qiu X, Zhang L.Specifying redundancy tactics as crosscutting concerns using aspect-oriented modeling[J].Frontiers of Computer Science,2014,8(6):977-995. |
| Click to display the text | |
| [19] | Di Nalate M, Stankovic J A.Dynamic end-to-end guarantees in distributed real time systems[C]//Proceedings Real-Time System Symposium.Piscataway,NJ:IEEE Press,1994:216-227. |
| Click to display the text |
