AADL端對端數(shù)據(jù)流一致性驗證方法

王 凱，畢海濱

(1.南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016；2.江南計算技術(shù)研究所 第三處，江蘇 無錫 214083)

0 引 言

在針對實時系統(tǒng)[1]的OSATE[2]建模過程中，數(shù)據(jù)和事件的傳輸通過數(shù)據(jù)流完成。一條完整的數(shù)據(jù)流通常由一個數(shù)據(jù)采集器開始，流經(jīng)中間組件(進(jìn)程組件)，到控制器結(jié)束。數(shù)據(jù)傳輸過程具有一定的時效性，系統(tǒng)會因為數(shù)據(jù)流不能及時到達(dá)而失效。

AADL標(biāo)準(zhǔn)的制定者PETER提出影響數(shù)據(jù)流時延的因素主要有四點[3]：組件本身的計算時延；不同組件間的傳輸時延；數(shù)據(jù)采樣速率和設(shè)備端口上數(shù)據(jù)隊列的處理方式；傳輸協(xié)議對于數(shù)據(jù)等待隊列的處理方式。作者在理論層面上全面分析了時延的影響因素，但只是選取了AADL屬性集合中的Latency屬性作為分析的依據(jù)，對端對端的數(shù)據(jù)流做了簡單的模擬。LEE Su-Young[4]基于進(jìn)程組件中的周期和非周期線程給出了數(shù)據(jù)流的最優(yōu)時延與最差時延的計算公式，但對于系統(tǒng)的調(diào)度并沒有給出分析依據(jù)，例如多線程的優(yōu)先級。譙婷婷等[5]通過實例給出了數(shù)據(jù)流分析的結(jié)果，但沒有給出一個通用的解決方案。文獻(xiàn)[6-7]將AADL模型轉(zhuǎn)換成時間自動機(jī)等模型來進(jìn)行性質(zhì)的等價驗證，用CPS進(jìn)行描述，用PDA工具進(jìn)行流性質(zhì)驗證，不過少有提及調(diào)度對端對端數(shù)據(jù)流的影響。

文中以數(shù)據(jù)流時延特性為研究目標(biāo)，建立數(shù)據(jù)流到Prolog的轉(zhuǎn)換，對于流經(jīng)線程的數(shù)據(jù)流，結(jié)合調(diào)度模型對多線程優(yōu)先級的考慮，針對單一型數(shù)據(jù)流及混合型數(shù)據(jù)流驗證了實時系統(tǒng)端對端數(shù)據(jù)流的一致性。

1 AADL端對端數(shù)據(jù)流及一致性定義

端對端的數(shù)據(jù)流[8](end to end flow)描述系統(tǒng)內(nèi)部數(shù)據(jù)和事件的傳遞路徑。AADL中完整的端對端數(shù)據(jù)流定義應(yīng)包含兩個部分：流聲明(flow specification)以及流實現(xiàn)(flow implementation)。

1.1 端對端數(shù)據(jù)流聲明

流聲明依附在組件的聲明中完成，定義從組件的輸入到輸出的邏輯路徑。流的基本要素為flow source(流源)、flow sink(流匯)和flow path(流路徑)。其中flow source和flow sink是組件features定義下的端口(ports)、端口組(ports group)或者共享參數(shù)(parameter)，flow path是flow source和flow sink間的連接。

1.2 端對端數(shù)據(jù)流實現(xiàn)

與流的聲明一樣，流的實現(xiàn)依附在組件的實現(xiàn)(implementation)中，通過組件與子組件、子組件與子組件的串聯(lián)，形成了從輸入端口到達(dá)輸出端口的串行序列，確切描述了組件內(nèi)部數(shù)據(jù)的流向。AADL定義規(guī)定，可以建立數(shù)據(jù)端口(data port)到數(shù)據(jù)、事件端口(event port}或數(shù)據(jù)事件端口(event data port)的連接，而事件端口僅可以和事件端口單向連接，事件端口向數(shù)據(jù)或者數(shù)據(jù)事件端口的連接是不允許的，例如流路徑能夠從任意類型的流入端口流向不同類型的端口(從數(shù)據(jù)端口流向事件端口)。

一個端對端的數(shù)據(jù)流Fp的定義可以描述為一個六元組，F(xiàn)p={F,fs,fd,Po,Co,La}。其中，F(xiàn)為作用于組件內(nèi)部的數(shù)據(jù)流，其表達(dá)式為F={Po×Po,La}，端對端的數(shù)據(jù)流也可表述為Fp={F×F,fs,fd}；fs∈F，表示flow source，數(shù)據(jù)流的起點；fd∈F，表示flow sink，是數(shù)據(jù)流的終點；Po為端口組件的集合，Po={data port,event port,eventdata port}，代表數(shù)據(jù)端口、事件端口和事件數(shù)據(jù)端口；Co={Po×Po,φ'}，表示不同組件間的端口連接的集合，φ'為連接約束的條件，禁止event port指向data port或event port，而其他指向的連接都是合法的；La表示Latency屬性的集合，它作用于F和Co。

1.3 數(shù)據(jù)流時延相關(guān)屬性

在不考慮組件本身是線程的情況下，計算整個端對端數(shù)據(jù)流時延時，與其直接相關(guān)的因素是Latency屬性[9-10]。Latency屬性代表數(shù)據(jù)流在端口間最長的時間消耗。在AADL的屬性集合中，定義了與數(shù)據(jù)流時延直接相關(guān)的屬性Latency，用于規(guī)定在流或連接上所允許的時間延遲，描述的對象包括數(shù)據(jù)流(flows)、連接(connections)等；屬性賦值為時間類型(整形加上時間單位)標(biāo)準(zhǔn)中給出的解釋。

1.4 端對端數(shù)據(jù)流的路徑一致性

定義1：端對端數(shù)據(jù)流的路徑一致性是指在一條完整的端對端數(shù)據(jù)流Fp中，針對數(shù)據(jù)流路徑(flow path)上的所有端口組件Po(普通端口組件Po滿足對應(yīng)的Compute_Execute_Time屬性)及端口間的數(shù)據(jù)流(數(shù)據(jù)流滿足對應(yīng)的Latency屬性)，任意一組時刻均滿足該數(shù)據(jù)流路徑上的所有約束。

圖1為汽艇自動駕駛儀系統(tǒng)的一部分。其中，speed_sensor是速度傳感器，數(shù)據(jù)從sensor_data端口經(jīng)過數(shù)據(jù)流到速度計算進(jìn)程speed_control的sensor_data端口，通過組件內(nèi)的數(shù)據(jù)流到達(dá)speed_control的command_data端口，最后經(jīng)數(shù)據(jù)流到達(dá)控制設(shè)備throttle的command_data端口，總共包含了四個數(shù)據(jù)端口，兩個組件間的數(shù)據(jù)流以及一個組件內(nèi)部的數(shù)據(jù)流。圖中，speed_sensor數(shù)據(jù)采集設(shè)備中的數(shù)據(jù)端口sensor.data通過數(shù)據(jù)流進(jìn)入下一個數(shù)據(jù)端口speed_control進(jìn)程中的sensor_data數(shù)據(jù)端口，這兩個組件間的數(shù)據(jù)流規(guī)定其Latency屬性為[5 ms,5 ms]，表示數(shù)據(jù)流時延在此時間范圍內(nèi)。而對于整個端口到端口的數(shù)據(jù)流，系統(tǒng)規(guī)定的時間時延(constraint)為35 ms，即對應(yīng)的從設(shè)備speed_sensor的sensor_data數(shù)據(jù)端口到設(shè)備throttle的command_data數(shù)據(jù)端口所消耗的時間應(yīng)在35 ms內(nèi)。如果存在一組時間取值滿足端對端的數(shù)據(jù)流在35 ms內(nèi)完成，則此一致性是滿足的，否則說明此端對端數(shù)據(jù)流路徑不一致(這里不考慮組件本身的Compute_Execute_Time，僅針對數(shù)據(jù)流時延討論)。

圖1 PBA子系統(tǒng)的數(shù)據(jù)計算及轉(zhuǎn)發(fā)

2 基于Prolog的單一型&混合型端對端數(shù)據(jù)流驗證方法

作為一種描述型語言，Prolog[11]只需描述問題中的對象和對象關(guān)系等已知的事實與規(guī)則，確定對象間的邏輯關(guān)系。給出待驗證的實時系統(tǒng)的事實與規(guī)則，作為Prolog的數(shù)據(jù)(即程序，數(shù)據(jù)與程序是統(tǒng)一的)進(jìn)行性質(zhì)驗證。為清楚地表述端對端數(shù)據(jù)流的Prolog事實，先將端對端數(shù)據(jù)流映射成狀態(tài)圖[12]，整條數(shù)據(jù)流映射為一個從初始化狀態(tài)到結(jié)束狀態(tài)的閉環(huán)。

根據(jù)端對端數(shù)據(jù)流所在的層級、是否流經(jīng)進(jìn)程下面具體的線程和調(diào)度程序是否對線程進(jìn)行派發(fā)，介紹基于Prolog的單一型端對端數(shù)據(jù)流及混合型端對端數(shù)據(jù)流[13](以下簡稱單一型數(shù)據(jù)流和混合型數(shù)據(jù)流)的驗證方法。

2.1 單一型數(shù)據(jù)流映射方法

單一型數(shù)據(jù)流是指在端對端數(shù)據(jù)流中，數(shù)據(jù)流經(jīng)組件時不考慮流向其子組件且流經(jīng)進(jìn)程組件時，不考慮線程任務(wù)本身的計算時延和調(diào)度器對線程調(diào)度的影響，設(shè)備對數(shù)據(jù)以及事件信號的發(fā)送和接收是即時的，數(shù)據(jù)流時延的產(chǎn)生僅考慮流屬性中定義的Latency。例如，圖1中的傳感器speed_sensor將采集的速度信息通過數(shù)據(jù)端口sensor_data發(fā)送給處理器speed_control，處理器通過sensor_data數(shù)據(jù)端口接收來自傳感器的速度信息，計算結(jié)束后通過數(shù)據(jù)端口command_data將速度信息傳遞給執(zhí)行器設(shè)備throttle的數(shù)據(jù)端口command_data，由速度執(zhí)行器對汽艇速度做出調(diào)整。在PBA子系統(tǒng)的端對端數(shù)據(jù)流中包含了四個數(shù)據(jù)端口，對應(yīng)這兩個組件間的數(shù)據(jù)流及一個組件內(nèi)部的數(shù)據(jù)流。對于此數(shù)據(jù)流，基于Prolog進(jìn)行驗證的規(guī)則如下所述：

(1)Po數(shù)據(jù)端口映射為基本狀態(tài)，按照實際系統(tǒng)中數(shù)據(jù)的流向串聯(lián)起來，在flow source前加入Start初始化狀態(tài)表述整條數(shù)據(jù)流的開始，且在flow sink后加入中止?fàn)顟B(tài)End作為驗證數(shù)據(jù)流路徑一致性的參考狀態(tài)。

(2)La表示數(shù)據(jù)流的Latency屬性，映射為數(shù)據(jù)端口間數(shù)據(jù)流時延信息，設(shè)置相應(yīng)的整形變量表示其時間約束。

(3)Co表示Po組件間的連接，映射到基本狀態(tài)信息中各狀態(tài)間的連接。

(4)F表示組件內(nèi)部的數(shù)據(jù)流，例如進(jìn)程中各個線程間的數(shù)據(jù)流交互。在單一型數(shù)據(jù)流不考慮調(diào)度策略的情況下，轉(zhuǎn)換為當(dāng)前組件的兩端口間的數(shù)據(jù)流，在基本狀態(tài)圖中表示為狀態(tài)間的連接。

PBA系統(tǒng)數(shù)據(jù)采集及轉(zhuǎn)發(fā)的單一型數(shù)據(jù)流映射為基本狀態(tài)信息如圖2所示。其中，PBA_Sensor_Data、PBA_Control_Data、PBA_Control_cmdData及PBA_Throttle_cmdData分別表示PBA子系統(tǒng)中的四個數(shù)據(jù)端口。在flow source前加入PBA_SpeedControl_Start初始化狀態(tài)及在flow end后加入PBA_SpeedControl_End中止?fàn)顟B(tài)。基本狀態(tài)間的數(shù)據(jù)流包含Latency時延信息。

圖2 單一型數(shù)據(jù)流的基本狀態(tài)圖

2.2 帶線程優(yōu)先級的混合型數(shù)據(jù)流映射方法

由數(shù)據(jù)采集器產(chǎn)生、流經(jīng)線程或者觸發(fā)非周期事件派發(fā)的數(shù)據(jù)流為混合型數(shù)據(jù)流。文中討論流經(jīng)線程的數(shù)據(jù)流的時延情況，接著介紹在基于線程優(yōu)先級調(diào)度策略下混合型數(shù)據(jù)流的驗證方法。

對PBA控制子系統(tǒng)在圖2中做了部分?jǐn)U充，如圖3所示。

圖3 包含計算線程的PBA子系統(tǒng)

數(shù)據(jù)流經(jīng)過進(jìn)程speed_control中的計算線程scale_speed_data，線程計算后將結(jié)果返回給進(jìn)程command_data接口，數(shù)據(jù)流時延的計算必須考慮計算線程的影響，而線程從調(diào)度系統(tǒng)派發(fā)到執(zhí)行結(jié)束受調(diào)度狀態(tài)的影響。

傳感器speed_sensor任務(wù)派發(fā)執(zhí)行后產(chǎn)生數(shù)據(jù)，經(jīng)過speed_sensor數(shù)據(jù)端口到達(dá)計算進(jìn)程的speed_control的數(shù)據(jù)端口sensor_data，并從sensor_data數(shù)據(jù)端口傳送到計算線程scale_speed_data中的sensor_data數(shù)據(jù)端口，對應(yīng)的兩條數(shù)據(jù)流的Latency屬性分別記為L1和L2。在到達(dá)計算線程scale_speed_data時，觸發(fā)了線程的派發(fā)，由于該線程的優(yōu)先級不高，得不到計算。圖4表示PBA控制子系統(tǒng)的數(shù)據(jù)流時延情況。虛線部分代表計算線程因優(yōu)先級不高而得不到計算的等待時間。隨后數(shù)據(jù)經(jīng)過Thread_Execution_time的計算時間后經(jīng)過數(shù)據(jù)流L3、L4到達(dá)執(zhí)行器throttle。

基于狀態(tài)圖的混合型數(shù)據(jù)流映射規(guī)則如下：

(1)Po數(shù)據(jù)端口映射為基本狀態(tài)，按照實際系統(tǒng)中數(shù)據(jù)的流向串聯(lián)起來，并在flow source前加入Start初始化狀態(tài)表述整條數(shù)據(jù)流的開始，并在flow sink后加入中止?fàn)顟B(tài)End作為驗證數(shù)據(jù)流路徑一致性的參考狀態(tài)。

(2)La表示數(shù)據(jù)流的Latency屬性，映射為數(shù)據(jù)端口間的數(shù)據(jù)流時延信息，設(shè)置相應(yīng)的整形變量表示其時間約束。

(3)Co表示Po組件間的連接，映射到基本狀態(tài)信息中各狀態(tài)間的連接。

圖4 PBA子系統(tǒng)時延分析示意圖

(4)F表示組件內(nèi)部的數(shù)據(jù)流，帶線程優(yōu)先級的混合型數(shù)據(jù)流中，按照線程優(yōu)先級的先后順序?qū)?yōu)先級高的線程(包含待計算的線程)映射為基本狀態(tài)加入組件內(nèi)部數(shù)據(jù)流中，由線程映射的基本狀態(tài)本身帶有線程計算所產(chǎn)生的時延Thread_Execution_time。

圖5為PBA子系統(tǒng)混合型數(shù)據(jù)流的基本狀態(tài)圖，其中PBA_ScaleThread線程為最高優(yōu)先級線程，映射為基本狀態(tài)且線程的執(zhí)行時間為8 μs。

圖5 混合型數(shù)據(jù)流的基本狀態(tài)圖

2.3 基于Prolog的數(shù)據(jù)流一致性驗證規(guī)則

針對端對端數(shù)據(jù)流Prolog驗證規(guī)則，利用minbordercons函數(shù)及maxbordercons函數(shù)描述1.4節(jié)中路徑一致性問題，下面給出函數(shù)具體實現(xiàn)及驗證表達(dá)。

使用minbordercons(A,B,T)函數(shù)來計算在給定的相鄰的基本狀態(tài)(即Po端口)A,B通信時所要花費的最短時間，并將計算后的結(jié)果賦值給T；minroutecons(A,B,T)函數(shù)則通過遞歸的思想計算端對端數(shù)據(jù)流路徑中組件之間的最短時延；fact(A,B,S,E)表示基本狀態(tài)圖中狀態(tài)節(jié)點的Prolog事實表達(dá)，A,B表示基本狀態(tài)，S,E表示基本狀態(tài)A,B間數(shù)據(jù)流時延的最小值及最大值；contraint(A,B,S)表示基本狀態(tài)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)來計算在給定的相鄰的基本狀態(tài)A,B所需要花費的最長時間，并將計算后的結(jié)果賦值給T；maxroutecons(A,B,T)函數(shù)則通過遞歸的思想計算端對端數(shù)據(jù)流路徑中組件之間最長時延，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.

結(jié)合上述函數(shù)，給出端到端數(shù)據(jù)流的路徑一致性驗證的Prolog表達(dá)。

fact(pba_start,sensor_data,0,0)

3 實例驗證與分析

本節(jié)將以汽艇自動駕駛儀(PBA)系統(tǒng)中的速度控制模塊為例，基于Prolog對AADL端對端的數(shù)據(jù)流進(jìn)行一致性驗證。

3.1 實例驗證

建立一個速度控制的AADL模型[14]，其功能是通過傳感器采集數(shù)據(jù)，通過數(shù)據(jù)端口發(fā)送給進(jìn)程的控制端口用來計算當(dāng)前的最佳艇速，最后通過數(shù)據(jù)端口傳輸給執(zhí)行器，用來改變當(dāng)前艇速。

針對速度控制子系統(tǒng)的單一型數(shù)據(jù)流及混合型數(shù)據(jù)流根據(jù)2.1及2.2提出的轉(zhuǎn)換方法，轉(zhuǎn)換后的基本狀態(tài)圖見圖4及圖5。下面給出單一型數(shù)據(jù)流及混合型數(shù)據(jù)流基本狀態(tài)圖的Prolog事實表達(dá)。

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節(jié)所提的路徑一致性驗證規(guī)則作為Prolog程序的輸入，得到的實驗數(shù)據(jù)如表1所示。

表1 數(shù)據(jù)流路徑一致性實驗結(jié)果

從表1中可以看到，PBA速度控制子系統(tǒng)中的單一型及混合型數(shù)據(jù)流完成數(shù)據(jù)傳輸需要消耗的時間分別為[23 ms,33 ms]和[27 ms,27 ms]，相對于整個系統(tǒng)的時延約束35 ms，數(shù)據(jù)流傳輸滿足了系統(tǒng)的要求。

3.2 實例分析

針對現(xiàn)有的實時系統(tǒng)時間一致性驗證的不足，提出了基于Prolog的AADL端對端數(shù)據(jù)流路徑一致性驗證方法。對端對端數(shù)據(jù)流進(jìn)行分類描述，給出端對端數(shù)據(jù)流路徑一致性Prolog驗證表達(dá)，最后通過SWI-Prolog進(jìn)行驗證。該方法和其他類似建模驗證方法在驗證方面的比較如表2所示，其中yes表示支持該性質(zhì)，no表示不支持。

表2 與現(xiàn)有方法的對比

從表2可以看出，針對現(xiàn)有的方法去驗證實時系統(tǒng)的時延特性時，現(xiàn)有方法很少能將其統(tǒng)一表述在同種方法中進(jìn)行驗證。

4 結(jié)束語

文中提出一種基于Prolog的端對端數(shù)據(jù)流分析方法。首先提出實時系統(tǒng)時延特性的路徑一致性問題，其次針對單一型數(shù)據(jù)流及混合型數(shù)據(jù)流特點設(shè)計了基于Prolog的驗證方法，最后通過將模型轉(zhuǎn)換成Prolog事實及路徑一致性轉(zhuǎn)換成Prolog規(guī)則，實現(xiàn)了對實時系統(tǒng)時延性質(zhì)的驗證。

[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].計算機(jī)應(yīng)用,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系統(tǒng)分析與設(shè)計[J].計算機(jī)應(yīng)用與軟件,2015,32(8):94-98.

[11] 李 娜,王湘云.基于謂詞邏輯的Prolog程序設(shè)計[J].西南大學(xué)學(xué)報:社會科學(xué)版,2009,35(6):48-52.

[12] 樊 波,袁國銘,周 萍,等.UML狀態(tài)圖在軟件工程設(shè)計中的應(yīng)用研究[J].微型電腦應(yīng)用,2015,31(11):36-37.

[13] 白海洋.基于UPPAAL的嵌入式系統(tǒng)AADL模型實時性驗證[D].南京:南京航空航天大學(xué),2014.

[14] 余晃晶,李仁發(fā),黃麗達(dá).基于AADL的汽車防滑控制系統(tǒng)可調(diào)度性分析[J].湖南大學(xué)學(xué)報:自然科學(xué)版,2012,39(3):43-47.