基于AADL的數(shù)據(jù)流轉(zhuǎn)換與驗(yàn)證

孫 健，徐 敏

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016)

基于AADL的數(shù)據(jù)流轉(zhuǎn)換與驗(yàn)證

孫 健，徐 敏

(南京航空航天大學(xué) 計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 210016)

AADL在嵌入式實(shí)時(shí)系統(tǒng)領(lǐng)域，支持系統(tǒng)軟、硬件結(jié)構(gòu)建模的同時(shí)又能對(duì)可靠性、實(shí)時(shí)性等非功能屬性進(jìn)行描述，可以在模型驅(qū)動(dòng)開(kāi)發(fā)過(guò)程中的早期模型建立階段，通過(guò)形式化的模型檢驗(yàn)方法對(duì)系統(tǒng)模型的關(guān)鍵屬性進(jìn)行驗(yàn)證，從而能夠及早地發(fā)現(xiàn)在設(shè)計(jì)過(guò)程中存在的潛在錯(cuò)誤，對(duì)保證系統(tǒng)實(shí)時(shí)性和提高開(kāi)發(fā)效率來(lái)說(shuō)都具有十分重要的意義。針對(duì)數(shù)據(jù)流時(shí)延特性問(wèn)題，文中提出將AADL數(shù)據(jù)流的分析形成數(shù)據(jù)流的形式化描述的方法，建立這種形式化描述到時(shí)間自動(dòng)機(jī)語(yǔ)義的映射關(guān)系作為映射法則的定義，并將時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換按單一和混合兩種類(lèi)型分別給出了轉(zhuǎn)換法則和轉(zhuǎn)換實(shí)例的說(shuō)明。在混合數(shù)據(jù)流轉(zhuǎn)換中，新建了非周期線程的模板，以支持?jǐn)?shù)據(jù)流的綜合分析。最后給出了數(shù)據(jù)流性質(zhì)驗(yàn)證的參考查詢(xún)語(yǔ)句，并對(duì)數(shù)據(jù)流轉(zhuǎn)換到的時(shí)間自動(dòng)機(jī)模型進(jìn)行了必要的實(shí)驗(yàn)檢驗(yàn)。

AADL；數(shù)據(jù)流時(shí)延；形式化描述；時(shí)間自動(dòng)機(jī)；性質(zhì)驗(yàn)證

1 概 述

在AADL模型中，數(shù)據(jù)流是數(shù)據(jù)和事件信息傳遞的通道。一條完整的端到端的數(shù)據(jù)流通常由一個(gè)采集器設(shè)備發(fā)出，傳遞給一個(gè)中間組件(例如線程組件)處理后，將處理結(jié)果傳遞給控制器做出響應(yīng)。在這個(gè)過(guò)程中，信號(hào)從采集到控制具有一定的時(shí)效性，若數(shù)據(jù)流的延遲過(guò)大，將會(huì)導(dǎo)致關(guān)鍵的數(shù)據(jù)不能及時(shí)送達(dá)或關(guān)鍵的任務(wù)不能按時(shí)觸發(fā)，從而影響整個(gè)系統(tǒng)的實(shí)時(shí)性[1-2]。

在AADL數(shù)據(jù)流時(shí)延特性的研究方面，AADL標(biāo)準(zhǔn)的制定者之一Peter Feiler在他的文章[3]中提出了影響數(shù)據(jù)流時(shí)延的因素及其分析方法，他指出影響數(shù)據(jù)流時(shí)延的因素主要有四點(diǎn)：

(1)線程或設(shè)備的計(jì)算；

(2)在不同組件之間傳輸?shù)臅r(shí)延；

(3)數(shù)據(jù)采樣速率和設(shè)備端口上數(shù)據(jù)隊(duì)列的處理方式；

(4)傳輸協(xié)議對(duì)于數(shù)據(jù)等待隊(duì)列的處理方式。

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

通過(guò)以上的分析，文中將數(shù)據(jù)流時(shí)延特性作為研究的目標(biāo)，構(gòu)建數(shù)據(jù)流到時(shí)間自動(dòng)機(jī)模型之間的轉(zhuǎn)換，對(duì)于流經(jīng)計(jì)算線程的數(shù)據(jù)流，可以結(jié)合調(diào)度模型的時(shí)間自動(dòng)機(jī)來(lái)進(jìn)行綜合分析，得到混合模式下數(shù)據(jù)流的時(shí)延及其模型的可調(diào)度性驗(yàn)證方法。通過(guò)以上方法來(lái)達(dá)成下列目的：

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

(2)數(shù)據(jù)流中各段所累加的時(shí)延能否滿(mǎn)足端到端數(shù)據(jù)流時(shí)延的設(shè)計(jì)要求；

(3)數(shù)據(jù)流流經(jīng)計(jì)算線程后，時(shí)延的要求能否滿(mǎn)足設(shè)計(jì)要求；

(4)數(shù)據(jù)流流向非周期線程的Dispatch端口時(shí)，在通過(guò)事件觸發(fā)線程的派發(fā)的情況下系統(tǒng)能否滿(mǎn)足可調(diào)度性設(shè)計(jì)要求。

2 AADL數(shù)據(jù)流

2.1 AADL簡(jiǎn)介

AADL可以詳細(xì)描述嵌入式系統(tǒng)性能相關(guān)的屬性，如可靠性、有效性、時(shí)間性、響應(yīng)性、吞吐量、安全性[1]。這些屬性使系統(tǒng)的設(shè)計(jì)者能夠完成對(duì)組件和系統(tǒng)的分析，例如系統(tǒng)的可調(diào)度性分析、粒度分析、可信性分析。

從這些分析中，設(shè)計(jì)者可以測(cè)評(píng)體系結(jié)構(gòu)的平衡和改變[5]。AADL滿(mǎn)足了安全關(guān)鍵嵌入式實(shí)時(shí)系統(tǒng)的相關(guān)特殊需要。

AADL的主要組件分為軟件組件和執(zhí)行平臺(tái)組件兩大類(lèi)。軟件組件主要包括數(shù)據(jù)、線程、進(jìn)程、子程序等；執(zhí)行平臺(tái)組件主要包括處理器、存儲(chǔ)器、總線、外設(shè)等。

作為AADL的執(zhí)行實(shí)體，線程可分為周期線程、非周期線程和零星線程三類(lèi)。它們的分派策略及其對(duì)外部事件的響應(yīng)各不相同。

2.2 數(shù)據(jù)流簡(jiǎn)介

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

在AADL的屬性集合中，定義了與數(shù)據(jù)流時(shí)延直接相關(guān)的屬性Latency，用來(lái)規(guī)定在流或者連接上所允許的時(shí)間延遲，描述的對(duì)象包括數(shù)據(jù)流(flows)、連接(connections)等。

2.3 數(shù)據(jù)流的形式化描述

fs：fs∈F，即flowsource，是端到端數(shù)據(jù)流的起點(diǎn)。

fd：fd∈F，即flowsink，是端到端數(shù)據(jù)流的終點(diǎn)。

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

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

2.4 時(shí)間自動(dòng)機(jī)理論

時(shí)間自動(dòng)機(jī)是在傳統(tǒng)的有限狀態(tài)自動(dòng)機(jī)的基礎(chǔ)上擴(kuò)充了時(shí)鐘、時(shí)鐘約束和不變條件而得到[8]。系統(tǒng)當(dāng)中定義的時(shí)鐘在一定取值范圍內(nèi)按照相同的速率同步連續(xù)的增長(zhǎng)，也可以在任意的時(shí)刻被復(fù)位為初始值0。系統(tǒng)的狀態(tài)轉(zhuǎn)移約束條件由時(shí)鐘和整型變量構(gòu)成，只有在時(shí)鐘滿(mǎn)足一定的條件下，狀態(tài)的轉(zhuǎn)移才能夠發(fā)生，而對(duì)于不變條件是對(duì)狀態(tài)停留在一個(gè)位置上的約束，滿(mǎn)足不變條件的情況下，時(shí)鐘才會(huì)在一個(gè)位置停留并持續(xù)增長(zhǎng)[9-13]。時(shí)間自動(dòng)機(jī)的系統(tǒng)由于引入了時(shí)鐘的概念后，對(duì)系統(tǒng)的時(shí)間概念具有了很強(qiáng)的表達(dá)能力，成為了描述實(shí)時(shí)系統(tǒng)模型的一個(gè)很好的工具。

作為一種形式化的方法，時(shí)間自動(dòng)機(jī)有其嚴(yán)格的定義，以下做以說(shuō)明[10]：

定義1：狀態(tài)轉(zhuǎn)移系統(tǒng)。

一個(gè)狀態(tài)轉(zhuǎn)移系統(tǒng)是一個(gè)四元組S=。其中：L是自動(dòng)機(jī)狀態(tài)的集合；I0(I0∈L)是一個(gè)初始的狀態(tài)；A是觸發(fā)轉(zhuǎn)移的事件集合；E?L×A×L是所有狀態(tài)轉(zhuǎn)移集合。

定義2：時(shí)鐘約束。

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

其中：x是一個(gè)時(shí)鐘變量；n是自然數(shù)集N中的一個(gè)常量。

定義3：時(shí)鐘解釋。

一個(gè)時(shí)鐘解釋是時(shí)鐘集合C到自然數(shù)集的映射，v:C→N。

定義4：時(shí)間自動(dòng)機(jī)。

時(shí)間自動(dòng)機(jī)是在有限狀態(tài)自動(dòng)機(jī)上擴(kuò)充了時(shí)鐘變量形成的，時(shí)鐘由整型變量代表，且所有的時(shí)鐘變量在自動(dòng)機(jī)中是同步遞增的[12-14]。一個(gè)時(shí)間自動(dòng)機(jī)可表示為一個(gè)六元組，TA=。其中：

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

I0：I0∈L，表示自動(dòng)機(jī)的初始位置，即初始狀態(tài)。

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

Var：一系列的變量集合。

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

I：不變條件(invariant)，是狀態(tài)轉(zhuǎn)移的約束函數(shù)的集合。

3 數(shù)據(jù)流到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換

3.1 單一數(shù)據(jù)流轉(zhuǎn)換方法

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

圖1 汽車(chē)防滑控制系統(tǒng)數(shù)據(jù)流模型圖

(1)Po→L，端口映射為基本狀態(tài)，根據(jù)數(shù)據(jù)的流向通過(guò)自動(dòng)機(jī)中的邊串聯(lián)起來(lái)，加入一個(gè)Start初始化狀態(tài)來(lái)表示流的開(kāi)始，并在最后加入中止?fàn)顟B(tài)End作為可達(dá)性驗(yàn)證的參考狀態(tài)。

(2)La→，時(shí)延對(duì)應(yīng)于時(shí)鐘變量和整型變量，一個(gè)端到端的流中設(shè)置了幾個(gè)分段的時(shí)延，就會(huì)設(shè)置幾個(gè)時(shí)鐘變量，同時(shí)設(shè)置相應(yīng)的整型變量來(lái)記錄約定的約束的值。

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

(4)流聲明中定義的F代表的是組件內(nèi)部的數(shù)據(jù)流，這部分的轉(zhuǎn)換方法與connection的轉(zhuǎn)換方法→相同。流實(shí)現(xiàn)中跨組件的flowpath的轉(zhuǎn)換中，Latency起到驗(yàn)證的作用，檢查flowpath內(nèi)部流的累加是否超過(guò)了設(shè)置的Latency值。為了能夠?qū)崿F(xiàn)這種轉(zhuǎn)換，文中設(shè)置了相應(yīng)的時(shí)鐘和整型變量。時(shí)鐘從flowpath的開(kāi)始狀態(tài)之前開(kāi)始計(jì)時(shí)，另外在flowpath終點(diǎn)端口的狀態(tài)之后加入了committed狀態(tài)，由終點(diǎn)端口的狀態(tài)指向該狀態(tài)。轉(zhuǎn)移條件為所設(shè)置時(shí)鐘的值小于或等于Latency的值，該committed狀態(tài)的后繼狀態(tài)為下一個(gè)端口狀態(tài)或end狀態(tài)。

對(duì)于圖1所示的模型，按照轉(zhuǎn)換規(guī)則轉(zhuǎn)換到的時(shí)間自動(dòng)機(jī)如圖2所示。

圖2 汽車(chē)防滑控制系統(tǒng)數(shù)據(jù)流時(shí)間自動(dòng)機(jī)

3.2 混合數(shù)據(jù)流轉(zhuǎn)換方法

在實(shí)際的系統(tǒng)中，數(shù)據(jù)的采集、發(fā)送往往是有一定周期或是觸發(fā)操作的，數(shù)據(jù)流向線程的計(jì)算也需要一定的時(shí)間，且這個(gè)時(shí)間與線程計(jì)算時(shí)間以及系統(tǒng)的調(diào)度情況都是密切相關(guān)的。將這種由采集設(shè)備產(chǎn)生、經(jīng)線程計(jì)算或者觸發(fā)非周期事件派發(fā)的數(shù)據(jù)流稱(chēng)為混合數(shù)據(jù)流。本節(jié)將首先分析信號(hào)源周期產(chǎn)生，并且經(jīng)過(guò)線程計(jì)算的數(shù)據(jù)流的時(shí)延情況，接著在調(diào)度模型中引入由事件引起的非周期派發(fā)的線程并對(duì)系統(tǒng)的調(diào)度情況加以分析。

在圖1所示的系統(tǒng)的基礎(chǔ)上，文中做了一些擴(kuò)充。數(shù)據(jù)流源頭的數(shù)據(jù)采集設(shè)備Sensor是周期工作的，同時(shí)數(shù)據(jù)信號(hào)的發(fā)送也是周期的。此外，數(shù)據(jù)流經(jīng)了一個(gè)計(jì)算線程，在設(shè)定的計(jì)算時(shí)間后，由輸出端口將結(jié)果返回?cái)?shù)據(jù)流，繼續(xù)傳遞給控制器。在這種情況下，數(shù)據(jù)流的時(shí)延必須要考慮到線程計(jì)算時(shí)間的因素，而線程從觸發(fā)到執(zhí)行結(jié)束的時(shí)間不是一個(gè)確定的值，它和系統(tǒng)所處的調(diào)度狀態(tài)有關(guān)。相對(duì)于單一數(shù)據(jù)流的轉(zhuǎn)換法則，混合數(shù)據(jù)流到時(shí)間自動(dòng)機(jī)的轉(zhuǎn)換法則擴(kuò)充為：

(1)Po0→TA，根據(jù)源端口Po0所在設(shè)備的派發(fā)形式和派發(fā)周期來(lái)設(shè)計(jì)一個(gè)數(shù)據(jù)產(chǎn)生器時(shí)間自動(dòng)機(jī)，通過(guò)同步通道通知數(shù)據(jù)流時(shí)間自動(dòng)機(jī)數(shù)據(jù)的產(chǎn)生。

(2)FT→，在指向線程輸入端口對(duì)應(yīng)狀態(tài)的邊上，通過(guò)設(shè)置數(shù)據(jù)流時(shí)間自動(dòng)機(jī)與非周期線程模板通信的同步通道來(lái)通知相應(yīng)線程派發(fā)，在從線程輸入端口狀態(tài)轉(zhuǎn)移到輸出端口狀態(tài)的邊上來(lái)設(shè)置線程執(zhí)行完成的接收同步信號(hào)。

根據(jù)擴(kuò)充的轉(zhuǎn)換法則，混合數(shù)據(jù)流的時(shí)間自動(dòng)機(jī)如圖3所示。

對(duì)于更復(fù)雜的情況來(lái)說(shuō)，由數(shù)據(jù)流連接起來(lái)的多個(gè)線程，線程之間具有級(jí)聯(lián)的關(guān)系，線程1產(chǎn)生的結(jié)果作為觸發(fā)線程2派發(fā)的信號(hào)，數(shù)據(jù)流時(shí)延和對(duì)調(diào)度模型的影響具有更大的不確定性。對(duì)于這種AADL模型的轉(zhuǎn)換仍然遵照上述的轉(zhuǎn)換規(guī)則，線程轉(zhuǎn)換成單獨(dú)的時(shí)間自動(dòng)機(jī)模板，數(shù)據(jù)流中按照基本的單一數(shù)據(jù)流轉(zhuǎn)換并加入同步通道和線程通信。

圖3 汽車(chē)防滑控制系統(tǒng)混合數(shù)據(jù)流時(shí)間自動(dòng)機(jī)

4 數(shù)據(jù)流性質(zhì)驗(yàn)證語(yǔ)句

數(shù)據(jù)流驗(yàn)證所關(guān)心的主要是流邏輯的正確性和設(shè)計(jì)所要求的時(shí)延特性，通過(guò)實(shí)際的自動(dòng)機(jī)的結(jié)束狀態(tài)和添加的端口檢查狀態(tài)的狀態(tài)可達(dá)性可以驗(yàn)證這兩個(gè)性質(zhì)。例如E<>SpeedControlFlow.Speedcontrol_Flow_End，若性質(zhì)滿(mǎn)足則說(shuō)明整個(gè)數(shù)據(jù)流在模型轉(zhuǎn)換的過(guò)程中已經(jīng)正確地連接起來(lái)，能夠形成邏輯上的通路，同時(shí)也證明了在該數(shù)據(jù)流上每個(gè)點(diǎn)對(duì)應(yīng)的時(shí)延約束是可以滿(mǎn)足的，單獨(dú)驗(yàn)證某端時(shí)延特性也可用E<>SpeedActuator_SpeedControl_In_Check。而調(diào)度模型中相關(guān)性質(zhì)的驗(yàn)證可以采用表1的驗(yàn)證查詢(xún)語(yǔ)句，數(shù)據(jù)流事件自動(dòng)機(jī)和非周期線程自動(dòng)機(jī)模板的引入并不對(duì)其性質(zhì)驗(yàn)證產(chǎn)生影響。

5 結(jié)束語(yǔ)

文中建立了AADL數(shù)據(jù)流到時(shí)間自動(dòng)機(jī)模型間的映射，利用模型轉(zhuǎn)換得到的時(shí)間自動(dòng)機(jī)分析了單一數(shù)據(jù)流和混合數(shù)據(jù)流的時(shí)延性質(zhì)，并與調(diào)度模型的時(shí)間自動(dòng)機(jī)結(jié)合構(gòu)成時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)，以更好地模擬AADL模型所描述的系統(tǒng)的運(yùn)轉(zhuǎn)情況，從而更準(zhǔn)確地驗(yàn)證可調(diào)度性和數(shù)據(jù)流時(shí)延的特性。最后給出了數(shù)據(jù)流時(shí)延性質(zhì)驗(yàn)證查詢(xún)語(yǔ)句的參考并設(shè)計(jì)了模型轉(zhuǎn)換方法檢驗(yàn)的實(shí)驗(yàn)，證明該轉(zhuǎn)換方法是可行的。

表1 模型可調(diào)度性性質(zhì)驗(yàn)證語(yǔ)句

文中在基于AADL的數(shù)據(jù)流轉(zhuǎn)換與驗(yàn)證中取得了一定的進(jìn)展，但數(shù)據(jù)流分析考慮的因素還較少，還不支持端口隊(duì)列上時(shí)延的分析，沒(méi)有考慮流經(jīng)周期線程的數(shù)據(jù)流。未來(lái)對(duì)數(shù)據(jù)流分析的工作將考慮更多的影響因素，從而實(shí)現(xiàn)更準(zhǔn)確的分析與驗(yàn)證。

[1] 楊志斌，皮 磊,胡 凱，等.復(fù)雜嵌入式實(shí)時(shí)系統(tǒng)體系結(jié)構(gòu)設(shè)計(jì)與分析語(yǔ)言:AADL[J].軟件學(xué)報(bào)，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] 譙婷婷,王 樂(lè),耶國(guó)棟.基于AADL的軟件可靠性驗(yàn)證[J].計(jì)算機(jī)應(yīng)用,2012，32(S2)：92-95.

[5] 劉 倩，桂盛霖，李 允,等.基于UPPAAL的AADL模型可調(diào)度性驗(yàn)證[J].計(jì)算機(jī)應(yīng)用，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].北京:清華大學(xué)出版社,2007.

[10] 童 超.基于時(shí)間自動(dòng)機(jī)的RBC控車(chē)流程研究[D].成都:西南交通大學(xué),2009.

[11] 朱雪陽(yáng)，唐稚松.基于時(shí)序邏輯的軟件體系結(jié)構(gòu)描述語(yǔ)言XYZ/ADL[J].軟件學(xué)報(bào)，2003，14(4)：713-720.

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

[13] 周清雷,姬莉霞,王艷梅.基于UPPAAL的實(shí)時(shí)系統(tǒng)模型驗(yàn)證[J].計(jì)算機(jī)應(yīng)用,2004,24(9):129-131.

[14] 余晃晶,李仁發(fā),黃麗達(dá).基于AADL的汽車(chē)防滑控制系統(tǒng)可調(diào)度性分析[J].湖南大學(xué)學(xué)報(bào):自然科學(xué)版,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

時(shí)間：2016-03-22

國(guó)家“973”重點(diǎn)基礎(chǔ)研究發(fā)展計(jì)劃項(xiàng)目(2014CB744900)

孫 健(1990-)，男，碩士研究生，研究方向?yàn)槿斯ぶ悄?；?敏，副教授，研究方向?yàn)槿斯ぶ悄?、軟件工程?/p>

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