AADL端对端数据流一致性验证方法

王 凯，毕海滨

(1.南京航空航天大学 计算机科学与技术学院，江苏 南京 210016；2.江南计算技术研究所 第三处，江苏 无锡 214083)

0 引 言

在针对实时系统[1]的OSATE[2]建模过程中，数据和事件的传输通过数据流完成。一条完整的数据流通常由一个数据采集器开始，流经中间组件(进程组件)，到控制器结束。数据传输过程具有一定的时效性，系统会因为数据流不能及时到达而失效。

AADL标准的制定者PETER提出影响数据流时延的因素主要有四点[3]：组件本身的计算时延；不同组件间的传输时延；数据采样速率和设备端口上数据队列的处理方式；传输协议对于数据等待队列的处理方式。作者在理论层面上全面分析了时延的影响因素，但只是选取了AADL属性集合中的Latency属性作为分析的依据，对端对端的数据流做了简单的模拟。LEE Su-Young[4]基于进程组件中的周期和非周期线程给出了数据流的最优时延与最差时延的计算公式，但对于系统的调度并没有给出分析依据，例如多线程的优先级。谯婷婷等[5]通过实例给出了数据流分析的结果，但没有给出一个通用的解决方案。文献[6-7]将AADL模型转换成时间自动机等模型来进行性质的等价验证，用CPS进行描述，用PDA工具进行流性质验证，不过少有提及调度对端对端数据流的影响。

文中以数据流时延特性为研究目标，建立数据流到Prolog的转换，对于流经线程的数据流，结合调度模型对多线程优先级的考虑，针对单一型数据流及混合型数据流验证了实时系统端对端数据流的一致性。

1 AADL端对端数据流及一致性定义

端对端的数据流[8](end to end flow)描述系统内部数据和事件的传递路径。AADL中完整的端对端数据流定义应包含两个部分：流声明(flow specification)以及流实现(flow implementation)。

1.1 端对端数据流声明

流声明依附在组件的声明中完成，定义从组件的输入到输出的逻辑路径。流的基本要素为flow source(流源)、flow sink(流汇)和flow path(流路径)。其中flow source和flow sink是组件features定义下的端口(ports)、端口组(ports group)或者共享参数(parameter)，flow path是flow source和flow sink间的连接。

1.2 端对端数据流实现

与流的声明一样，流的实现依附在组件的实现(implementation)中，通过组件与子组件、子组件与子组件的串联，形成了从输入端口到达输出端口的串行序列，确切描述了组件内部数据的流向。AADL定义规定，可以建立数据端口(data port)到数据、事件端口(event port}或数据事件端口(event data port)的连接，而事件端口仅可以和事件端口单向连接，事件端口向数据或者数据事件端口的连接是不允许的，例如流路径能够从任意类型的流入端口流向不同类型的端口(从数据端口流向事件端口)。

一个端对端的数据流Fp的定义可以描述为一个六元组，Fp={F,fs,fd,Po,Co,La}。其中，F为作用于组件内部的数据流，其表达式为F={Po×Po,La}，端对端的数据流也可表述为Fp={F×F,fs,fd}；fs∈F，表示flow source，数据流的起点；fd∈F，表示flow sink，是数据流的终点；Po为端口组件的集合，Po={data port,event port,eventdata port}，代表数据端口、事件端口和事件数据端口；Co={Po×Po,φ'}，表示不同组件间的端口连接的集合，φ'为连接约束的条件，禁止event port指向data port或event port，而其他指向的连接都是合法的；La表示Latency属性的集合，它作用于F和Co。

1.3 数据流时延相关属性

在不考虑组件本身是线程的情况下，计算整个端对端数据流时延时，与其直接相关的因素是Latency属性[9-10]。Latency属性代表数据流在端口间最长的时间消耗。在AADL的属性集合中，定义了与数据流时延直接相关的属性Latency，用于规定在流或连接上所允许的时间延迟，描述的对象包括数据流(flows)、连接(connections)等；属性赋值为时间类型(整形加上时间单位)标准中给出的解释。

1.4 端对端数据流的路径一致性

定义1：端对端数据流的路径一致性是指在一条完整的端对端数据流Fp中，针对数据流路径(flow path)上的所有端口组件Po(普通端口组件Po满足对应的Compute_Execute_Time属性)及端口间的数据流(数据流满足对应的Latency属性)，任意一组时刻均满足该数据流路径上的所有约束。

图1为汽艇自动驾驶仪系统的一部分。其中，speed_sensor是速度传感器，数据从sensor_data端口经过数据流到速度计算进程speed_control的sensor_data端口，通过组件内的数据流到达speed_control的command_data端口，最后经数据流到达控制设备throttle的command_data端口，总共包含了四个数据端口，两个组件间的数据流以及一个组件内部的数据流。图中，speed_sensor数据采集设备中的数据端口sensor.data通过数据流进入下一个数据端口speed_control进程中的sensor_data数据端口，这两个组件间的数据流规定其Latency属性为[5 ms,5 ms]，表示数据流时延在此时间范围内。而对于整个端口到端口的数据流，系统规定的时间时延(constraint)为35 ms，即对应的从设备speed_sensor的sensor_data数据端口到设备throttle的command_data数据端口所消耗的时间应在35 ms内。如果存在一组时间取值满足端对端的数据流在35 ms内完成，则此一致性是满足的，否则说明此端对端数据流路径不一致(这里不考虑组件本身的Compute_Execute_Time，仅针对数据流时延讨论)。

图1 PBA子系统的数据计算及转发

2 基于Prolog的单一型&混合型端对端数据流验证方法

作为一种描述型语言，Prolog[11]只需描述问题中的对象和对象关系等已知的事实与规则，确定对象间的逻辑关系。给出待验证的实时系统的事实与规则，作为Prolog的数据(即程序，数据与程序是统一的)进行性质验证。为清楚地表述端对端数据流的Prolog事实，先将端对端数据流映射成状态图[12]，整条数据流映射为一个从初始化状态到结束状态的闭环。

根据端对端数据流所在的层级、是否流经进程下面具体的线程和调度程序是否对线程进行派发，介绍基于Prolog的单一型端对端数据流及混合型端对端数据流[13](以下简称单一型数据流和混合型数据流)的验证方法。

2.1 单一型数据流映射方法

单一型数据流是指在端对端数据流中，数据流经组件时不考虑流向其子组件且流经进程组件时，不考虑线程任务本身的计算时延和调度器对线程调度的影响，设备对数据以及事件信号的发送和接收是即时的，数据流时延的产生仅考虑流属性中定义的Latency。例如，图1中的传感器speed_sensor将采集的速度信息通过数据端口sensor_data发送给处理器speed_control，处理器通过sensor_data数据端口接收来自传感器的速度信息，计算结束后通过数据端口command_data将速度信息传递给执行器设备throttle的数据端口command_data，由速度执行器对汽艇速度做出调整。在PBA子系统的端对端数据流中包含了四个数据端口，对应这两个组件间的数据流及一个组件内部的数据流。对于此数据流，基于Prolog进行验证的规则如下所述：

(1)Po数据端口映射为基本状态，按照实际系统中数据的流向串联起来，在flow source前加入Start初始化状态表述整条数据流的开始，且在flow sink后加入中止状态End作为验证数据流路径一致性的参考状态。

(2)La表示数据流的Latency属性，映射为数据端口间数据流时延信息，设置相应的整形变量表示其时间约束。

(3)Co表示Po组件间的连接，映射到基本状态信息中各状态间的连接。

(4)F表示组件内部的数据流，例如进程中各个线程间的数据流交互。在单一型数据流不考虑调度策略的情况下，转换为当前组件的两端口间的数据流，在基本状态图中表示为状态间的连接。

PBA系统数据采集及转发的单一型数据流映射为基本状态信息如图2所示。其中，PBA_Sensor_Data、PBA_Control_Data、PBA_Control_cmdData及PBA_Throttle_cmdData分别表示PBA子系统中的四个数据端口。在flow source前加入PBA_SpeedControl_Start初始化状态及在flow end后加入PBA_SpeedControl_End中止状态。基本状态间的数据流包含Latency时延信息。

图2 单一型数据流的基本状态图

2.2 带线程优先级的混合型数据流映射方法

由数据采集器产生、流经线程或者触发非周期事件派发的数据流为混合型数据流。文中讨论流经线程的数据流的时延情况，接着介绍在基于线程优先级调度策略下混合型数据流的验证方法。

对PBA控制子系统在图2中做了部分扩充，如图3所示。

图3 包含计算线程的PBA子系统

数据流经过进程speed_control中的计算线程scale_speed_data，线程计算后将结果返回给进程command_data接口，数据流时延的计算必须考虑计算线程的影响，而线程从调度系统派发到执行结束受调度状态的影响。

传感器speed_sensor任务派发执行后产生数据，经过speed_sensor数据端口到达计算进程的speed_control的数据端口sensor_data，并从sensor_data数据端口传送到计算线程scale_speed_data中的sensor_data数据端口，对应的两条数据流的Latency属性分别记为L1和L2。在到达计算线程scale_speed_data时，触发了线程的派发，由于该线程的优先级不高，得不到计算。图4表示PBA控制子系统的数据流时延情况。虚线部分代表计算线程因优先级不高而得不到计算的等待时间。随后数据经过Thread_Execution_time的计算时间后经过数据流L3、L4到达执行器throttle。

基于状态图的混合型数据流映射规则如下：

(1)Po数据端口映射为基本状态，按照实际系统中数据的流向串联起来，并在flow source前加入Start初始化状态表述整条数据流的开始，并在flow sink后加入中止状态End作为验证数据流路径一致性的参考状态。

(2)La表示数据流的Latency属性，映射为数据端口间的数据流时延信息，设置相应的整形变量表示其时间约束。

(3)Co表示Po组件间的连接，映射到基本状态信息中各状态间的连接。

图4 PBA子系统时延分析示意图

(4)F表示组件内部的数据流，带线程优先级的混合型数据流中，按照线程优先级的先后顺序将优先级高的线程(包含待计算的线程)映射为基本状态加入组件内部数据流中，由线程映射的基本状态本身带有线程计算所产生的时延Thread_Execution_time。

图5为PBA子系统混合型数据流的基本状态图，其中PBA_ScaleThread线程为最高优先级线程，映射为基本状态且线程的执行时间为8 μs。

图5 混合型数据流的基本状态图

2.3 基于Prolog的数据流一致性验证规则

针对端对端数据流Prolog验证规则，利用minbordercons函数及maxbordercons函数描述1.4节中路径一致性问题，下面给出函数具体实现及验证表达。

使用minbordercons(A,B,T)函数来计算在给定的相邻的基本状态(即Po端口)A,B通信时所要花费的最短时间，并将计算后的结果赋值给T；minroutecons(A,B,T)函数则通过递归的思想计算端对端数据流路径中组件之间的最短时延；fact(A,B,S,E)表示基本状态图中状态节点的Prolog事实表达，A,B表示基本状态，S,E表示基本状态A,B间数据流时延的最小值及最大值；contraint(A,B,S)表示基本状态A,B间的时间约束。

Prolog程序如下：

minbordercons(A,B,T)：-not(A=B),

fact(A,B,S1,_),

fact(B,_,S2,_),

TisS1+S2.

minroutecons(A,B,T)：-

not(A=B), fact(A,B,S1,_),

fact(B,_,S2,_),

TisS1+S2.

minroutecons(A,B,T)：-

fact(A,Z,S1,_),

minroutecons(Z,B,T1),

TisS1+T1.

使用maxbordercons(A,B,T)来计算在给定的相邻的基本状态A,B所需要花费的最长时间，并将计算后的结果赋值给T；maxroutecons(A,B,T)函数则通过递归的思想计算端对端数据流路径中组件之间最长时延，Prolog程序如下：

maxbordercons(A,B,T)：-

not(A=B),fact(A,B,_,E1),

fact(B,_,_,E2),

TisE1+E2.

maxroutecons(A,B,T)：-

not(A=B),fact(A,B,_,E1),

fact(B,_,_,E2),

TisE1+E2.

maxroutecons(A,B,T)：-

fact(A,Z,_,E1),

maxroutecons(Z,B,_,T1),

TisE1+T1.

结合上述函数，给出端到端数据流的路径一致性验证的Prolog表达。

fact(pba_start,sensor_data,0,0)

3 实例验证与分析

本节将以汽艇自动驾驶仪(PBA)系统中的速度控制模块为例，基于Prolog对AADL端对端的数据流进行一致性验证。

3.1 实例验证

建立一个速度控制的AADL模型[14]，其功能是通过传感器采集数据，通过数据端口发送给进程的控制端口用来计算当前的最佳艇速，最后通过数据端口传输给执行器，用来改变当前艇速。

针对速度控制子系统的单一型数据流及混合型数据流根据2.1及2.2提出的转换方法，转换后的基本状态图见图4及图5。下面给出单一型数据流及混合型数据流基本状态图的Prolog事实表达。

fact(pba_start,sensor_data,0,0)

fact(sensor_data,control_data,5,5)

fact(control_data,control_cmddata,10,20)

fact(control_cmddata,throttle_cmddata,8,8)

fact(throttle_cmddata,pba_end,0,0)

constraint(pba_start,pba_end,35)

fact(pba_start,sensor_data,0,0)

fact(sensor_data,control_sendata,5,5)

fact(control_sendata,scaleThread_sendata,3,3)

fact(scaleThread_sendata,scaleThread,8,8)

fact(scaleThread,scaleThread_cmddata,0,0)

fact(scaleThread_cmddata,control_cmddata,3,3)

fact(control_cmddata,throttle_cmddata,8,8)

fact(throttle_cmddata,pba_end,0,0)

constraint(pba_start,pba_end,35)

将上述事实与第2节所提的路径一致性验证规则作为Prolog程序的输入，得到的实验数据如表1所示。

表1 数据流路径一致性实验结果

从表1中可以看到，PBA速度控制子系统中的单一型及混合型数据流完成数据传输需要消耗的时间分别为[23 ms,33 ms]和[27 ms,27 ms]，相对于整个系统的时延约束35 ms，数据流传输满足了系统的要求。

3.2 实例分析

针对现有的实时系统时间一致性验证的不足，提出了基于Prolog的AADL端对端数据流路径一致性验证方法。对端对端数据流进行分类描述，给出端对端数据流路径一致性Prolog验证表达，最后通过SWI-Prolog进行验证。该方法和其他类似建模验证方法在验证方面的比较如表2所示，其中yes表示支持该性质，no表示不支持。

表2 与现有方法的对比

从表2可以看出，针对现有的方法去验证实时系统的时延特性时，现有方法很少能将其统一表述在同种方法中进行验证。

4 结束语

文中提出一种基于Prolog的端对端数据流分析方法。首先提出实时系统时延特性的路径一致性问题，其次针对单一型数据流及混合型数据流特点设计了基于Prolog的验证方法，最后通过将模型转换成Prolog事实及路径一致性转换成Prolog规则，实现了对实时系统时延性质的验证。

[1] HAI N T,SINGHOFF F,RUBINI S,et al.Instruction cache in hard real-time systems：modeling and integration in scheduling analysis tools with AADL[C]//International conference on embedded and ubiquitous computing.[s.l.]:IEEE,2014：104-111.

[2] LOUKIL S,KALLEL S,ZALILA B,et al.AO4AADL:aspect oriented extension for AADL[J].Central European Journal of Computer Science,2013,3(2)：43-68.

[3] ZHAO Y,MA D.Embedded real-time system modeling and analysis using AADL[C]//International conference on networking and information technology.[s.l.]:IEEE,2010:247-251.

[4] LEE S Y,MALLET F,SIMONE R D.Dealing with AADL end-to-end flow latency with UML MARTE[C]//International conference on engineering of complex computer systems.[s.l.]:IEEE Computer Society,2008：228-233.

[5] 谯婷婷,王 乐,耶国栋.基于AADL的软件可靠性验证[J].计算机应用,2012,32(S2)：92-95.

[6] ZHU Y,DONG Y,MA C,et al.A methodology of model-based testing for AADL flow latency in CPS[C]//5th international conference on secure software integration & reliability improvement companion.[s.l.]:IEEE,2011：99-105.

[7] YU H,YANG Y.Latency analysis of automobile ABS based on AADL[C]//International conference on industrial control and electronics engineering.[s.l.]:[s.n.],2012:1835-1838.

[8] SKELIN M,GEILEN M,CATTHOOR F,et al.Worst-case latency analysis of SDF-based parametrized dataflow MoCs[C]//Proceedings of design and architectures for signal and image processing.[s.l.]:IEEE,2015:1-6.

[9] MAGNON A.Time-latency,time-flow and universal blue-print[M].[s.l.]:[s.n.],2015:197-217.

[10] 朱晨曦,张立臣,罗崇伟.基于AADL的CPS系统分析与设计[J].计算机应用与软件,2015,32(8):94-98.

[11] 李 娜,王湘云.基于谓词逻辑的Prolog程序设计[J].西南大学学报:社会科学版,2009,35(6):48-52.

[12] 樊 波,袁国铭,周 萍,等.UML状态图在软件工程设计中的应用研究[J].微型电脑应用,2015,31(11):36-37.

[13] 白海洋.基于UPPAAL的嵌入式系统AADL模型实时性验证[D].南京:南京航空航天大学,2014.

[14] 余晃晶,李仁发,黄丽达.基于AADL的汽车防滑控制系统可调度性分析[J].湖南大学学报:自然科学版,2012,39(3):43-47.