孫 健，徐 敏

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

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

孫 健，徐 敏

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

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

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

0 引 言

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

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

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

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

1 AADL與UPPAAL

1.1 AADL概述

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

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

1.2 時(shí)間自動(dòng)機(jī)與UPPAAL概述

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

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

下面根據(jù)時(shí)間自動(dòng)機(jī)的定義，做如下說(shuō)明[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)移的集合。

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

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

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

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

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

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

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

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

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

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

1.2.2 驗(yàn)證工具UPPAAL

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

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

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

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

2.1 非可搶占調(diào)度策略下的時(shí)間自動(dòng)機(jī)設(shè)計(jì)

(1)線程模板。

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

圖1 非可搶占調(diào)度策略下周期線程時(shí)間自動(dòng)機(jī)模板

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

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

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

圖2 非可搶占調(diào)度策略下調(diào)度器時(shí)間自動(dòng)機(jī)模板

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

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

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

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

2.2 可搶占調(diào)度策略下時(shí)間自動(dòng)機(jī)設(shè)計(jì)

(1)線程模板。

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

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

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

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

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

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

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

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

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

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

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

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

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

[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)度性驗(yàn)證[J].計(jì)算機(jī)應(yīng)用，2009,29(7)：1820-1824.

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

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

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

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

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

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

[14] 周清雷,姬莉霞,王艷梅.基于UPPAAL的實(shí)時(shí)系統(tǒng)模型驗(yàn)證[J].計(jì)算機(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

時(shí)間：2016-02-18

國(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.20160218.1630.032.html

TP302

A

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

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