孫 健，徐 敏

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

基于AADL的嵌入式系統(tǒng)可調(diào)度性驗證

孫 健，徐 敏

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

AADL近年來在嵌入式實時系統(tǒng)領(lǐng)域得到了廣泛的應(yīng)用，相對于其他語言能夠更好地描述系統(tǒng)的非功能屬性，同時支持系統(tǒng)軟硬件建模，在基于模型驅(qū)動的開發(fā)方法下對系統(tǒng)進(jìn)行建模和分析，用形式化的方法對系統(tǒng)的相關(guān)屬性進(jìn)行驗證，從而可以在設(shè)計階段發(fā)現(xiàn)錯誤，對保證系統(tǒng)的安全運行和開發(fā)效率的提高有著重要意義。對于驗證AADL模型可調(diào)度性的問題，文中利用時間自動機理論，根據(jù)AADL調(diào)度模型和時間自動機模型的語義相似性，將AADL模型轉(zhuǎn)換成時間自動機模型，并設(shè)計轉(zhuǎn)換插件，通過Eclipse插件開發(fā)技術(shù)將其集成到AADL建模與分析工具OSATE中。最后在UPPAAL工具中對轉(zhuǎn)換后的時間自動機模型進(jìn)行模擬和驗證，利用相關(guān)性質(zhì)驗證語句等價地對原模型的可調(diào)度性進(jìn)行驗證。

嵌入式系統(tǒng)；體系結(jié)構(gòu)分析設(shè)計語言；時間自動機；模型轉(zhuǎn)換；UPPAAL；實時性

0 引 言

對于安全關(guān)鍵的嵌入式系統(tǒng)來說，系統(tǒng)的非功能屬性跟功能屬性一樣重要，都需要得到滿足[1-2]?；谀Ｐ万?qū)動的方法可對系統(tǒng)設(shè)計和安全性分析采用一致的模型，該模型貫穿整個開發(fā)過程[3]。在系統(tǒng)設(shè)計階段，通過對模型分析和驗證，發(fā)現(xiàn)錯誤來提高系統(tǒng)的安全性，保證系統(tǒng)能夠正常運行，從而提高開發(fā)效率。

體系結(jié)構(gòu)分析設(shè)計語言(Architecture Analysis and Design Language，AADL)近年來在航空電子領(lǐng)域以及安全性分析等方面得到了廣泛應(yīng)用，是一種符合模型驅(qū)動思想的建模和分析語言，在2004年由SAE基于MetaH和UML提出，并發(fā)布為SAEAS5506標(biāo)準(zhǔn)，能對系統(tǒng)的軟硬件進(jìn)行建模。隨著AADL的廣泛應(yīng)用以及對內(nèi)容的擴展，與AADL相關(guān)的研究工作及其工具的開發(fā)日益成為研究熱點。

時間自動機建模與分析工具UPPAAL近年來在實時系統(tǒng)中得到廣泛應(yīng)用，具有建模功能靈活、驗證效率高等特點，也在AADL建模與分析中得到了嘗試[4-5]。其中，Johnsen在文獻(xiàn)[6]中提出用UPPAAL進(jìn)行建模，并在模擬器和驗證器中對模型進(jìn)行模擬和驗證，且模型的調(diào)度策略是固定優(yōu)先級的；劉倩等使用UPPAAL對AADL非可搶占調(diào)度模型設(shè)計了時間自動機[7]。上述研究存在的問題是調(diào)度策略單一，沒有考慮到線程切換中的時間消耗，從而對于實際的AADL模型不能很好地進(jìn)行模擬，且其考慮的問題還停在了對自動機的建模和驗證上，而對于AADL模型轉(zhuǎn)換為時間自動機模型，以及轉(zhuǎn)換插件的設(shè)計都還沒較多的涉及。

針對上述問題，利用時間自動機理論，根據(jù)AADL調(diào)度模型和時間自動機模型的語義相似性，將AADL模型轉(zhuǎn)換成時間自動機模型，并設(shè)計轉(zhuǎn)換插件，在UPPAAL工具中對轉(zhuǎn)換后的時間自動機模型進(jìn)行模擬和驗證，利用相關(guān)性質(zhì)驗證語句等價地對原模型的可調(diào)度性進(jìn)行驗證。

1 AADL與UPPAAL

1.1 AADL概述

在AADL中，組件通過類型和實現(xiàn)聲明來定義[8]。一個組件類型說明定義了一個組件的接口元素以及外部可觀察屬性(即與其他組件、流程規(guī)范和內(nèi)部屬性值之間交互點的特性)。一個組件實現(xiàn)的聲明定義了一個組件內(nèi)部結(jié)構(gòu)的子組件、子組件連接、子程序調(diào)用、模式、流實現(xiàn)以及屬性。組件被分為應(yīng)用程序軟件，執(zhí)行平臺和復(fù)合組件，屬性集和附件庫使得設(shè)計者能夠擴展語言和自定義一個AADL規(guī)范來符合項目或特定區(qū)域的需求。

組件在特定的組件類別中聲明為類型和實現(xiàn)，有三組不同的組件類別：應(yīng)用軟件、執(zhí)行平臺和復(fù)合。一個AADL組件類型聲明建立了一個組件的外部可見特性[7]。例如，一個聲明指定了一個線程組件的接口，一個組件類型聲明由一個定義句子和描述性的子句組成，特征(features)是組件的接口，流(flows)指定信息流的不同抽象通道，屬性(properties)定義組件的固有特性，每個組件類別都有預(yù)定義的屬性(如一個線程的執(zhí)行時間)。組件的實現(xiàn)就是用來描述一個組件的內(nèi)部結(jié)構(gòu)，一個組件實現(xiàn)包括的子句主要有：流，屬性，模式和子組件。流(flows)代表組件類型里流規(guī)范的實現(xiàn)或者端到端的流分析(流從一個子組件開始，經(jīng)過零個或更多子組件并在另一個子組件結(jié)束)；模式(modes)是對組件、連接及屬性值的配置，表示一個系統(tǒng)或組件可達(dá)到的操作狀態(tài)；屬性(properties)定義組件的固有特性，每個組件的實現(xiàn)都有預(yù)定義的屬性。

1.2 時間自動機與UPPAAL概述

1.2.1 時間自動機理論

時間自動機[9]理論最早是在1992年由Alur R提出，在有限狀態(tài)自動機上擴充了時鐘、時鐘約束及不變條件而得到。時間自動機被提出是實時系統(tǒng)建模自動機理論的擴展，從此時間自動機理論及其驗證工具一直是計算機科學(xué)研究的一個密集領(lǐng)域。一個時間自動機是一個配備了一組有限時鐘的有限自動機，時鐘是時間的連續(xù)的實值函數(shù)，精確地記錄時間的流逝。所有時鐘以相同的速度前進(jìn)，即它們是同步的，實時系統(tǒng)行為使用時間自動機來捕獲，通過設(shè)置時鐘以及用常數(shù)比較時鐘讀數(shù)[10]。所有時鐘都有和時間相關(guān)的相同的衍生物，且都被假定為一個相同的定義。

下面根據(jù)時間自動機的定義，做如下說明[11]：

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

將狀態(tài)轉(zhuǎn)移系統(tǒng)形式化為四元組。其中：T為轉(zhuǎn)移系統(tǒng)中的狀態(tài)集合；t0(t0∈T)為初始狀態(tài)；P為觸發(fā)狀態(tài)發(fā)生轉(zhuǎn)移的事件集合；E?T×P×T為所有狀態(tài)轉(zhuǎn)移的集合。

在一個系統(tǒng)中，一個狀態(tài)在觸發(fā)事件的作用下發(fā)生狀態(tài)轉(zhuǎn)移，若一個狀態(tài)到另一個狀態(tài)的轉(zhuǎn)移發(fā)生則稱該狀態(tài)到另一狀態(tài)是可到達(dá)的，而從初始狀態(tài)開始，所有可到達(dá)其他狀態(tài)的轉(zhuǎn)移構(gòu)成了狀態(tài)空間。

定義2：時鐘約束。

把φ(C)作為時鐘約束集合，其中C為時鐘變量集，定義時鐘約束集合為：

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

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

定義3：時鐘解釋。

時鐘解釋v:C→N表示集合C到自然數(shù)的映射。

對于一個δ∈R，R表示的時鐘解釋是對于集合C中的每一個時鐘變量x的賦值為v(x)+δ；對于一個δ∈R，δ·v表示的時鐘解釋是對C中的每個時鐘變量x賦值為δ·v(x)；對于X?C，v[X:=0]表示對于滿足x∈X的時鐘x復(fù)位為0，其余時鐘保持增長。

定義4：時間自動機。

在有限狀態(tài)自動機的基礎(chǔ)上，通過增加時鐘變量的概念形成了時間自動機，其中時鐘為整型變量，并且所有的時鐘變量是同步遞增的[12-14]。一個時間自動機可以表示為一個六元組，TA=。其中：T為有向圖中有窮的位置(location)集合；t0為自動機的初始狀態(tài)；C為時鐘集合，默認(rèn)從0開始，不斷自增加1，可以隨時被重新賦值；V為所有變量的集合；E為有向圖中所有邊(edge)的集合；I為狀態(tài)轉(zhuǎn)移約束函數(shù)的集合，即不變條件(invariant)。

1.2.2 驗證工具UPPAAL

UPPAAL[7]是一個基于約束求解和動態(tài)技術(shù)的，用來進(jìn)行實時系統(tǒng)建模、仿真和驗證的工具，它可以將系統(tǒng)建模成一系列具有有限控制結(jié)構(gòu)和實值時鐘的非確定性的進(jìn)程，并通過共享變量進(jìn)行通信。典型的應(yīng)用領(lǐng)域包括實時控制器和特別的通信協(xié)議，時間方面是十分關(guān)鍵的，所以在設(shè)計方面，主要是通過探索系統(tǒng)的狀態(tài)空間來檢查不變和可達(dá)性。

UPPAAL工具的兩個設(shè)計標(biāo)準(zhǔn)是效率和易于使用，可達(dá)性分析的限制對于工具的模型檢查器的效率至關(guān)重要。對效率的另一個關(guān)鍵是結(jié)合符號技術(shù)的動態(tài)搜索技術(shù)的應(yīng)用，減少為處理和解決簡單約束的驗證問題。為了方便建模和調(diào)試，UPPAAL模型檢查器會自動生成一個診斷跟蹤，來解釋為什么一個屬性滿足(或不滿足)一個系統(tǒng)描述，由模型檢查器生成的診斷跟蹤可以使用模擬器來圖形化顯示。

2 AADL可調(diào)度模型轉(zhuǎn)換與驗證

為了驗證實時系統(tǒng)AADL模型中的可調(diào)度性，利用時間自動機形式化方法。首先分析AADL模型，將與系統(tǒng)調(diào)度相關(guān)的屬性信息提取出來，抽象出調(diào)度模型。在非可搶占及可搶占調(diào)度策略下，分別設(shè)計了線程和調(diào)度器時間自動機模板(以下簡稱模板)，并利用TCTL驗證語句對UPPAAL中的時間自動機模型進(jìn)行可調(diào)度性驗證。最后設(shè)計了從AADL調(diào)度模型到時間自動機模型的轉(zhuǎn)換插件，并自動調(diào)用UPPAAL打開模型對相關(guān)性質(zhì)進(jìn)行驗證。

2.1 非可搶占調(diào)度策略下的時間自動機設(shè)計

(1)線程模板。

線程是執(zhí)行的主體，線程組件也是通過線程模板來進(jìn)行轉(zhuǎn)換，在線程模擬的過程中，用標(biāo)號id來區(qū)分，在非可搶占策略下設(shè)計了如圖1所示的周期線程時間自動機模板。

圖1 非可搶占調(diào)度策略下周期線程時間自動機模板

如圖1所示，模板中有四個狀態(tài)，分別為初始化狀態(tài)(Initialized)、準(zhǔn)備狀態(tài)(Ready)、錯誤狀態(tài)(Error)及運行狀態(tài)(Running)。Initialized狀態(tài)表示線程創(chuàng)建成功且處于等待被派發(fā)的狀態(tài)，其中不變條件cl<=Period代表線程處于Initialized狀態(tài)的條件為局部時鐘小于等于周期；Ready表示線程按照優(yōu)先級的高低進(jìn)入到等待隊列，等待被處理器執(zhí)行；Running狀態(tài)對應(yīng)于線程狀態(tài)轉(zhuǎn)換機制中的Compute(計算)狀態(tài)，表示線程正在被運行；Error狀態(tài)對應(yīng)于線程狀態(tài)轉(zhuǎn)換機制中的Recover(恢復(fù))狀態(tài)，表示線程由于超時而進(jìn)入到一種死鎖狀態(tài)，且所有的狀態(tài)轉(zhuǎn)移在該狀態(tài)下都會中止。

(2)調(diào)度器模板。

根據(jù)并發(fā)系統(tǒng)的特點，即線程會根據(jù)調(diào)度策略通過調(diào)度器來決定其運行狀況，于是在調(diào)度器時間自動機模板的設(shè)計過程中，利用同步通道以及全局變量與線程進(jìn)行通信，對組件調(diào)度屬性進(jìn)行模擬，設(shè)計的調(diào)度器模板如圖2所示。

圖2 非可搶占調(diào)度策略下調(diào)度器時間自動機模板

從圖中可以看出，調(diào)度器模板有如下五個狀態(tài)：等待狀態(tài)(Awaiting)、調(diào)度狀態(tài)(Schedule)、運行狀態(tài)(Running)、完成狀態(tài)(Completed)、超時狀態(tài)(MissedDeadline)。其中調(diào)度狀態(tài)、完成狀態(tài)為限制狀態(tài)，即不考慮時間的流逝，為中間狀態(tài)。Awaiting狀態(tài)表示在處理器中沒有要調(diào)度執(zhí)行的線程；Schedule是一種中間狀態(tài)，調(diào)度器會在有線程被派發(fā)時進(jìn)入到該狀態(tài)；Running狀態(tài)表示線程的運行狀態(tài)，模擬線程在處理器上的運行；Completed狀態(tài)表示線程運行完畢，進(jìn)入該狀態(tài)的條件為線程實際運行時間與需要的最大運行時間相等；MissedDeadline狀態(tài)表示線程運行超時，沒有在截止時間之前完成運行，當(dāng)系統(tǒng)進(jìn)入到此狀態(tài)便會發(fā)生死鎖，即該系統(tǒng)不可調(diào)度。

(3)帶有線程切換時間下的非可搶占調(diào)度器模板。

線程在切換時產(chǎn)生了時間的消耗，并在模型中用Thread_Swap_Execution_Time表示線程切換過程所產(chǎn)生的時間消耗。因此本節(jié)擴展了模板，用switch_clock表示切換時鐘，用switch_clock<=switchTime模擬某狀態(tài)的時間切換。

擴充后的模板中，switchTime若為0，則表示該調(diào)度器模板不考慮切換時間，但在實際情況中，新增加的判斷條件可能會帶來很大的影響和負(fù)擔(dān)，因此將其轉(zhuǎn)換到對應(yīng)的模板顯得尤為重要。

2.2 可搶占調(diào)度策略下時間自動機設(shè)計

(1)線程模板。

相對于非可搶占調(diào)度策略，在可搶占調(diào)度策略下，周期線程時間自動機模板增加了一個Preempted狀態(tài)。該狀態(tài)表示線程在運行時被更高優(yōu)先級的線程搶占后停止運行，等到更高優(yōu)先線程運行完之后，該線程恢復(fù)運行，返回到Running狀態(tài)，其中該狀態(tài)上的截止時鐘是持續(xù)增長的。

(2)調(diào)度器模板。

由于引入了線程的搶占、恢復(fù)等操作，在可搶占調(diào)度策略下，調(diào)度器模板的復(fù)雜程度相對來說要大些。在非可搶占的調(diào)度器模板基礎(chǔ)上，該模板增加了兩個狀態(tài)Schedule1和Preemption。其中：Schedule1是一種中間狀態(tài)，調(diào)度器在有線程被派發(fā)時會進(jìn)入到此狀態(tài)，同時線程會在調(diào)度器中按優(yōu)先級高低排成一個隊列ready_q；Preemeption狀態(tài)表示有新線程派發(fā)時Schedule1決定執(zhí)行可搶占調(diào)度，并按優(yōu)先級由高到低依次進(jìn)入運行狀態(tài)，且被搶占的線程會進(jìn)入到被搶占狀態(tài)。

(3)帶有線程切換時間下的可搶占調(diào)度器模板。

線程在可搶占調(diào)度策略下，因搶占而產(chǎn)生時間的消耗，所以線程在恢復(fù)到執(zhí)行狀態(tài)時被搶占時間的計算會有所不同。

2.3 模型轉(zhuǎn)換器的工具實現(xiàn)

對于模型的自動轉(zhuǎn)換，通過Eclipse插件開發(fā)技術(shù)設(shè)計了轉(zhuǎn)換插件，并將其集成到了AADL建模與分析工具OSATE中，實現(xiàn)了AADL模型到時間自動機模型的自動轉(zhuǎn)換。插件以實例化的AADL模型作為輸入，通過文件解析，轉(zhuǎn)換生成時間自動機模型文件和性質(zhì)驗證查詢文件，自動調(diào)用UPPAAL工具打開模型進(jìn)行可調(diào)度性驗證。

2.4 可調(diào)度性驗證

文中使用UPPAAL(時間自動機建模與驗證工具)來驗證設(shè)計的時間自動機模型，從而對AADL調(diào)度模型進(jìn)行等價的可調(diào)度性驗證。UPPAAL內(nèi)含有模擬器和驗證器，在模擬器里可以觀察時間自動機的狀態(tài)轉(zhuǎn)移，且可用單步或連續(xù)的方式，同時可觀察狀態(tài)序列的變化，從而模擬系統(tǒng)的運行。從前面的介紹中可知，在UPPAAL中，模型驗證時所使用的理論是自動機可達(dá)性驗證理論。同時在驗證器中使用了時序邏輯TCTL來進(jìn)行相關(guān)屬性的驗證，其性質(zhì)查詢語言包括狀態(tài)公式和路徑公式。而文中在驗證調(diào)度模型的可調(diào)度性中，用到的主要語句見表1。

3 結(jié)束語

文中利用時間自動機的形式化檢驗方法，設(shè)計了AADL調(diào)度模型到時間自動機模型的轉(zhuǎn)換方法，在UPPAAL工具中對時間自動機模型進(jìn)行模擬和驗證，利用相關(guān)驗證語句，等價地驗證原模型可調(diào)度性。同時設(shè)計了不同調(diào)度策略下的線程和調(diào)度器模板以及自動轉(zhuǎn)換插件，并將其集成到工具OSATE中，使得嵌入式實時系統(tǒng)的建模、轉(zhuǎn)換以及驗證實現(xiàn)一體化。

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

對基于時間自動機的AADL模型驗證工作雖然取得了一定進(jìn)展，但考慮調(diào)度策略影響因素時，所關(guān)心的還不是很全面，如目前還不支持多處理器和EDF調(diào)度算法。在未來的研究工作中，需進(jìn)一步考慮影響系統(tǒng)調(diào)度的因素，從而使得分析和驗證的效果更加全面。

[1] Krishna C M.Real-time systems[M].[s.l.]:John Wiley & Sons,Inc.,1999.

[2] Peled D.Software reliability methods[M].Berlin:Springer,2001.

[3] Selic B.The pragmatics of model-driven development[J].IEEE Software,2003,20(5):19-25.

[4] Bj?rnander S, Seceleanu C.A formal analysis framework for AADL[J].Journal of Science and Technology,2011,49(5):1-13.

[5] Bae K,?lveczky P C,Meseguer J,et al.The SynchAADL2 Maude tool[M].Berlin:Springer,2012.

[6] Johnsen A.Architecture-based verification of dependable embedded systems[D].Sweden:M?lardalen University,2013.

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

[8] 楊志斌，皮 磊,胡 凱,等.復(fù)雜嵌入式實時系統(tǒng)體系結(jié)構(gòu)設(shè)計與分析語言:AADL[J].軟件學(xué)報，2010，21(5)：899-915.

[9] Alur R.Timed automata[M]//Computer aided verification.Berlin:Springer,1999.

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

[11] 童 超.基于時間自動機的RBC控車流程研究[D].成都:西南交通大學(xué)，2009.

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

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

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

Schedulability Verification of Embedded System Based on AADL

SUN Jian，XU Min

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

AADL has been widely used in embedded real-time system in recent years.Compared with other languages,it can better describe the system non functional attributes,and also support the software and hardware modeling of the system.AADL can model and analyze the system based on the model driven development method,and verify relevant properties using formal method.Error can be found in the design phase,and it has great significance to ensure the safe operation of the system and improve the efficiency of development.For verifying AADL model schedulability problem,according to the semantics similarity of AADL scheduling model and timed automata model,the theory of timed automata is used to convert AADL model to timed automata model,and integrate conversion plug-in into the AADL modeling and analysis tool OSATE through the development of Eclipse plug-in technology.Finally,the converted timed automaton model in the UPPAAL tool is simulated and verified,using the related verification statement to verify the schedulability of the original model.

embedded system;AADL;timed automata;model transformation;UPPAAL;real-time

2015-06-09

2015-09-15

時間：2016-02-18

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

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

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

TP302

A

1673-629X(2016)03-0023-04

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