基于AADL的數據流轉換與驗證

孫 健，徐 敏

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

基于AADL的數據流轉換與驗證

孫 健，徐 敏

(南京航空航天大學 計算機科學與技術學院，江蘇 南京 210016)

AADL在嵌入式實時系統領域，支持系統軟、硬件結構建模的同時又能對可靠性、實時性等非功能屬性進行描述，可以在模型驅動開發過程中的早期模型建立階段，通過形式化的模型檢驗方法對系統模型的關鍵屬性進行驗證，從而能夠及早地發現在設計過程中存在的潛在錯誤，對保證系統實時性和提高開發效率來說都具有十分重要的意義。針對數據流時延特性問題，文中提出將AADL數據流的分析形成數據流的形式化描述的方法，建立這種形式化描述到時間自動機語義的映射關系作為映射法則的定義，并將時間自動機的轉換按單一和混合兩種類型分別給出了轉換法則和轉換實例的說明。在混合數據流轉換中，新建了非周期線程的模板，以支持數據流的綜合分析。最后給出了數據流性質驗證的參考查詢語句，并對數據流轉換到的時間自動機模型進行了必要的實驗檢驗。

AADL；數據流時延；形式化描述；時間自動機；性質驗證

1 概 述

在AADL模型中，數據流是數據和事件信息傳遞的通道。一條完整的端到端的數據流通常由一個采集器設備發出，傳遞給一個中間組件(例如線程組件)處理后，將處理結果傳遞給控制器做出響應。在這個過程中，信號從采集到控制具有一定的時效性，若數據流的延遲過大，將會導致關鍵的數據不能及時送達或關鍵的任務不能按時觸發，從而影響整個系統的實時性[1-2]。

在AADL數據流時延特性的研究方面，AADL標準的制定者之一Peter Feiler在他的文章[3]中提出了影響數據流時延的因素及其分析方法，他指出影響數據流時延的因素主要有四點：

(1)線程或設備的計算；

(2)在不同組件之間傳輸的時延；

(3)數據采樣速率和設備端口上數據隊列的處理方式；

(4)傳輸協議對于數據等待隊列的處理方式。

盡管時延的影響因素得到了全面分析，但Peter Feiler也只是選取了AADL屬性集合中的Latency屬性作為其分析的依據，同時在其開發的OSATE插件中，利用該屬性對模型的數據流做了簡單的模擬，并將模擬計算得出的時延結果與預期時延進行比較。另外，在Lee Su-Young等[2]的研究中，結合了周期和非周期線程對于數據流的影響，分析給出了線程的數據流的時延與線程的計算時間、截止時間等的關系，得出了最優時延與最差時延的計算公式。但是這種計算沒有考慮到實際的系統調度對數據流中數據流向的影響，是很不精確的。譙婷婷等[4]基于一個飛行控制系統的實例給出了流分析的結果，但沒有給出一般的方法或通用的解決方案。

通過以上的分析，文中將數據流時延特性作為研究的目標，構建數據流到時間自動機模型之間的轉換，對于流經計算線程的數據流，可以結合調度模型的時間自動機來進行綜合分析，得到混合模式下數據流的時延及其模型的可調度性驗證方法。通過以上方法來達成下列目的：

(1)檢查數據流的完整性，即從源端口到目的端口能否形成完整的邏輯通路；

(2)數據流中各段所累加的時延能否滿足端到端數據流時延的設計要求；

(3)數據流流經計算線程后，時延的要求能否滿足設計要求；

(4)數據流流向非周期線程的Dispatch端口時，在通過事件觸發線程的派發的情況下系統能否滿足可調度性設計要求。

2 AADL數據流

2.1 AADL簡介

AADL可以詳細描述嵌入式系統性能相關的屬性，如可靠性、有效性、時間性、響應性、吞吐量、安全性[1]。這些屬性使系統的設計者能夠完成對組件和系統的分析，例如系統的可調度性分析、粒度分析、可信性分析。

從這些分析中，設計者可以測評體系結構的平衡和改變[5]。AADL滿足了安全關鍵嵌入式實時系統的相關特殊需要。

AADL的主要組件分為軟件組件和執行平臺組件兩大類。軟件組件主要包括數據、線程、進程、子程序等；執行平臺組件主要包括處理器、存儲器、總線、外設等。

作為AADL的執行實體，線程可分為周期線程、非周期線程和零星線程三類。它們的分派策略及其對外部事件的響應各不相同。

2.2 數據流簡介

AADL模型的組件是通過流(flow)來進行連接的，端到端的流(end to end flow)描述了系統內部數據和事件的抽象信息路徑。與AADL中的組件一樣，完整的flow定義包含兩個部分：流聲明(flow specification)和流實現(flow implementation)[5-6]。流聲明在組件聲明中完成，它定義了從組件輸入到輸出的邏輯路徑，含有三種標記類型：flow source(流的起源)、flow sink(流的終點)和 flow path(流的路徑)。流實現在組件實現中完成[7]，通過串聯組件與子組件、子組件與子組件之間的連接，形成了從輸入端口到輸出端口之間的串行序列，描述了組件中確切的數據流向。與流聲明對應，流實現也有三種類型，其定義方式與流聲明略有不同，每個實現都代表一條路徑。端到端的數據流(end to end flow)作為流實現中的特例，實現了跨組件之間數據流的連接，它的起點是flow source，終點是flow sink，中間可以串聯多個組件之間的flow implementation和 connections。

在AADL的屬性集合中，定義了與數據流時延直接相關的屬性Latency，用來規定在流或者連接上所允許的時間延遲，描述的對象包括數據流(flows)、連接(connections)等。

2.3 數據流的形式化描述

fs：fs∈F，即flowsource，是端到端數據流的起點。

fd：fd∈F，即flowsink，是端到端數據流的終點。

Po：端口組件的集合，其中Po={dataport,eventport,eventport}。

La：Latency屬性的集合，作用于F和Co。

2.4 時間自動機理論

時間自動機是在傳統的有限狀態自動機的基礎上擴充了時鐘、時鐘約束和不變條件而得到[8]。系統當中定義的時鐘在一定取值范圍內按照相同的速率同步連續的增長，也可以在任意的時刻被復位為初始值0。系統的狀態轉移約束條件由時鐘和整型變量構成，只有在時鐘滿足一定的條件下，狀態的轉移才能夠發生，而對于不變條件是對狀態停留在一個位置上的約束，滿足不變條件的情況下，時鐘才會在一個位置停留并持續增長[9-13]。時間自動機的系統由于引入了時鐘的概念后，對系統的時間概念具有了很強的表達能力，成為了描述實時系統模型的一個很好的工具。

作為一種形式化的方法，時間自動機有其嚴格的定義，以下做以說明[10]：

定義1：狀態轉移系統。

一個狀態轉移系統是一個四元組S=。其中：L是自動機狀態的集合；I0(I0∈L)是一個初始的狀態；A是觸發轉移的事件集合；E?L×A×L是所有狀態轉移集合。

定義2：時鐘約束。

φ:=x??n|φ1∧φ2

其中：x是一個時鐘變量；n是自然數集N中的一個常量。

定義3：時鐘解釋。

一個時鐘解釋是時鐘集合C到自然數集的映射，v:C→N。

定義4：時間自動機。

時間自動機是在有限狀態自動機上擴充了時鐘變量形成的，時鐘由整型變量代表，且所有的時鐘變量在自動機中是同步遞增的[12-14]。一個時間自動機可表示為一個六元組，TA=。其中：

L：有窮的位置(location)集合。

I0：I0∈L，表示自動機的初始位置，即初始狀態。

C：時鐘的集合(Clock)，時鐘默認從0開始，不斷自增加1，可以在任意時刻被重新賦值。

Var：一系列的變量集合。

E：邊(Edge)的集合，E?L×G×Act×U×L。其中：G代表約束條件的集合，只有滿足約束條件，轉移才會發生；Act=I∪O，構成了觸發轉移的使能條件；U是對時鐘變量或者整型變量的更新操作。

I：不變條件(invariant)，是狀態轉移的約束函數的集合。

3 數據流到時間自動機的轉換

3.1 單一數據流轉換方法

單一數據流指的是所有數據端口都在同一層級的組件之間，數據不流向其子組件，且不受線程計算及系統任務調度的影響，設備對數據及其事件信號的發送和接收是即時的，數據流時延的產生只考慮流屬性中所定義的Latency。例如，圖1為汽車防滑控制系統部分AADL模型[14]，Sensor表示一個輪速傳感器，它實時采集汽車車輪的轉動速度，通過Speed_Out數據端口發送給處理器Processor，處理器通過Speed_In端口接收到數據，計算后通過SpeedControl_Out端口將控制信息發送給速度控制器SpeedActuator的接收端口SpeedControl_In，對速度做出實時調整。在這個控制系統中，可以看出一個端到端的數據流包含了四個數據端口，兩個組件之間端口的連接以及一個組件內部的數據流，所連接的部分均處在同一個組件層級。該數據流到時間自動機的轉換規則闡述如下。

圖1 汽車防滑控制系統數據流模型圖

(1)Po→L，端口映射為基本狀態，根據數據的流向通過自動機中的邊串聯起來，加入一個Start初始化狀態來表示流的開始，并在最后加入中止狀態End作為可達性驗證的參考狀態。

(2)La→，時延對應于時鐘變量和整型變量，一個端到端的流中設置了幾個分段的時延，就會設置幾個時鐘變量，同時設置相應的整型變量來記錄約定的約束的值。

(3)→，每個connection的時延轉換為三部分：一個時鐘賦值、一個轉移條件以及一個不變條件。時鐘賦值在端口對應狀態的進入條件中設置，將其時鐘置為0。轉移條件在由連接起點端口狀態轉移到終點端口狀態的邊上進行設置，判斷條件為clock==latency，表示連接上數據的傳遞在Latency設置的時間點上完成。相應的不變條件為clock<=latency，是對轉移前狀態的約束。

(4)流聲明中定義的F代表的是組件內部的數據流，這部分的轉換方法與connection的轉換方法→相同。流實現中跨組件的flowpath的轉換中，Latency起到驗證的作用，檢查flowpath內部流的累加是否超過了設置的Latency值。為了能夠實現這種轉換，文中設置了相應的時鐘和整型變量。時鐘從flowpath的開始狀態之前開始計時，另外在flowpath終點端口的狀態之后加入了committed狀態，由終點端口的狀態指向該狀態。轉移條件為所設置時鐘的值小于或等于Latency的值，該committed狀態的后繼狀態為下一個端口狀態或end狀態。

對于圖1所示的模型，按照轉換規則轉換到的時間自動機如圖2所示。

圖2 汽車防滑控制系統數據流時間自動機

3.2 混合數據流轉換方法

在實際的系統中，數據的采集、發送往往是有一定周期或是觸發操作的，數據流向線程的計算也需要一定的時間，且這個時間與線程計算時間以及系統的調度情況都是密切相關的。將這種由采集設備產生、經線程計算或者觸發非周期事件派發的數據流稱為混合數據流。本節將首先分析信號源周期產生，并且經過線程計算的數據流的時延情況，接著在調度模型中引入由事件引起的非周期派發的線程并對系統的調度情況加以分析。

在圖1所示的系統的基礎上，文中做了一些擴充。數據流源頭的數據采集設備Sensor是周期工作的，同時數據信號的發送也是周期的。此外，數據流經了一個計算線程，在設定的計算時間后，由輸出端口將結果返回數據流，繼續傳遞給控制器。在這種情況下，數據流的時延必須要考慮到線程計算時間的因素，而線程從觸發到執行結束的時間不是一個確定的值，它和系統所處的調度狀態有關。相對于單一數據流的轉換法則，混合數據流到時間自動機的轉換法則擴充為：

(1)Po0→TA，根據源端口Po0所在設備的派發形式和派發周期來設計一個數據產生器時間自動機，通過同步通道通知數據流時間自動機數據的產生。

(2)FT→，在指向線程輸入端口對應狀態的邊上，通過設置數據流時間自動機與非周期線程模板通信的同步通道來通知相應線程派發，在從線程輸入端口狀態轉移到輸出端口狀態的邊上來設置線程執行完成的接收同步信號。

根據擴充的轉換法則，混合數據流的時間自動機如圖3所示。

對于更復雜的情況來說，由數據流連接起來的多個線程，線程之間具有級聯的關系，線程1產生的結果作為觸發線程2派發的信號，數據流時延和對調度模型的影響具有更大的不確定性。對于這種AADL模型的轉換仍然遵照上述的轉換規則，線程轉換成單獨的時間自動機模板，數據流中按照基本的單一數據流轉換并加入同步通道和線程通信。

圖3 汽車防滑控制系統混合數據流時間自動機

4 數據流性質驗證語句

數據流驗證所關心的主要是流邏輯的正確性和設計所要求的時延特性，通過實際的自動機的結束狀態和添加的端口檢查狀態的狀態可達性可以驗證這兩個性質。例如E<>SpeedControlFlow.Speedcontrol_Flow_End，若性質滿足則說明整個數據流在模型轉換的過程中已經正確地連接起來，能夠形成邏輯上的通路，同時也證明了在該數據流上每個點對應的時延約束是可以滿足的，單獨驗證某端時延特性也可用E<>SpeedActuator_SpeedControl_In_Check。而調度模型中相關性質的驗證可以采用表1的驗證查詢語句，數據流事件自動機和非周期線程自動機模板的引入并不對其性質驗證產生影響。

5 結束語

文中建立了AADL數據流到時間自動機模型間的映射，利用模型轉換得到的時間自動機分析了單一數據流和混合數據流的時延性質，并與調度模型的時間自動機結合構成時間自動機網絡，以更好地模擬AADL模型所描述的系統的運轉情況，從而更準確地驗證可調度性和數據流時延的特性。最后給出了數據流時延性質驗證查詢語句的參考并設計了模型轉換方法檢驗的實驗，證明該轉換方法是可行的。

表1 模型可調度性性質驗證語句

文中在基于AADL的數據流轉換與驗證中取得了一定的進展，但數據流分析考慮的因素還較少，還不支持端口隊列上時延的分析，沒有考慮流經周期線程的數據流。未來對數據流分析的工作將考慮更多的影響因素，從而實現更準確的分析與驗證。

[1] 楊志斌，皮 磊,胡 凱，等.復雜嵌入式實時系統體系結構設計與分析語言:AADL[J].軟件學報，2010，21(5)：899-915.

[2]LeeSY,MalletF,deSimoneR.DealingwithAADLend-to-endflowlatencywithUMLMARTE[C]//Procof13thIEEEinternationalconferenceonengineeringofcomplexcomputersystems.[s.l.]:IEEE,2008.

[3]FeilerPH,HanssonJ.FlowlatencyanalysiswiththeArchitectureAnalysis&DesignLanguage(AADL)[R].[s.l.]:[s.n.],2008.

[4] 譙婷婷,王 樂,耶國棟.基于AADL的軟件可靠性驗證[J].計算機應用,2012，32(S2)：92-95.

[5] 劉 倩，桂盛霖，李 允,等.基于UPPAAL的AADL模型可調度性驗證[J].計算機應用，2009,29(7)：1820-1824.

[6]JohnsenA.Architecture-basedverificationofdependableembeddedsystems[D].Sweden:M?lardalenUniversity,2013.

[7]FeilerPH,LewisBA,VestalS.TheSAEArchitectureAnalysis&DesignLanguage(AADL)astandardforengineeringperformancecriticalsystems[C]//Computeraidedcontrolsystemdesign,2006IEEEinternationalconferenceoncontrolapplications,2006IEEEInternationalsymposiumonintelligentcontrol.Munich,Germany:IEEE,2006:1206-1211.

[8]AlurR.Timedautomata[M]//Computeraidedverification.Berlin:Springer,1999.

[9] 徐仁佐.軟件可靠性工程[M].北京:清華大學出版社,2007.

[10] 童 超.基于時間自動機的RBC控車流程研究[D].成都:西南交通大學,2009.

[11] 朱雪陽，唐稚松.基于時序邏輯的軟件體系結構描述語言XYZ/ADL[J].軟件學報，2003，14(4)：713-720.

[12] 李振松,顧 斌.基于UPPAAL的AADL行為模型驗證方法研究[J].計算機科學，2012，39(2)：159-161.

[13] 周清雷,姬莉霞,王艷梅.基于UPPAAL的實時系統模型驗證[J].計算機應用,2004,24(9):129-131.

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

Transformation and Verification of Data Flows Based on AADL

SUN Jian，XU Min

(School of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics, Nanjing 210016,China)

AADL supports structural modeling for software and hardware,and imports non-functional attributes description such as real-time and reliability in embedded real-time system.During the process of MDD (Model-Driven Development),it is of great significance for ensuring the system real-time performance and improving the efficiency of system development to find potential design problems on critical aspects in the model design stage.In order to analyze the flow latency of AADL models,a method is proposed taking the analysis of data flows of AADL to form a formal description of data flows.The mapping relationship from formal description to time automaton semantics is regarded as the definition of mapping rules.On building the timed automata of date flows,methods and samples are given to transform both simple and mixed flows into timed automata.In the transformation of mixed flows,a template of non-periodic thread is presented to support the comprehensive analysis of data flows.At last the reference query statements is given to verify the properties of the data flows,and the necessary experimental tests of time automaton model converted from data flows are carried out.

AADL;data flow latency;formal description;time automata;property verification

2015-07-19

2015-10-20

時間：2016-03-22

國家“973”重點基礎研究發展計劃項目(2014CB744900)

孫 健(1990-)，男，碩士研究生，研究方向為人工智能；徐 敏，副教授，研究方向為人工智能、軟件工程。

http://www.cnki.net/kcms/detail/61.1450.TP.20160322.1522.084.html

TP302

A

1673-629X(2016)04-0041-05

10.3969/j.issn.1673-629X.2016.04.009