李 靜 沈?qū)幟?白海洋 周培云

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

伴隨微電子、通信等技術(shù)的飛速發(fā)展，嵌入式實(shí)時(shí)系統(tǒng)廣泛應(yīng)用于航空航天、工業(yè)控制等任務(wù)的關(guān)鍵領(lǐng)域中，為了提升系統(tǒng)開發(fā)效率和可靠性，基于模型驅(qū)動(dòng)架構(gòu)(model driven architecture，MDA)［1］思想的體系結(jié)構(gòu)分析與設(shè)計(jì)語(yǔ)言AADL被應(yīng)用到嵌入式實(shí)時(shí)系統(tǒng)的建模與模型驗(yàn)證中.它能更好地支持嵌入式系統(tǒng)軟硬件一體化的建模，同時(shí)對(duì)系統(tǒng)的可靠性等非功能屬性進(jìn)行描述［2］.其中，可調(diào)度性是指系統(tǒng)的調(diào)度策略和資源狀況能否滿足所有任務(wù)的執(zhí)行需求，在任務(wù)的截止時(shí)間之內(nèi)完成執(zhí)行且不發(fā)生死鎖，是嵌入式實(shí)時(shí)系統(tǒng)正確執(zhí)行的最基本性質(zhì).

AADL 模型驗(yàn)證與分析主要采用仿真和形式化方法.ADeS 作為一種系統(tǒng)行為的仿真工具，目前還不支持子程序調(diào)用、行為附件的仿真［3］.Singhoff 等［4］采用仿真方法對(duì)可調(diào)度性進(jìn)行分析，但處理復(fù)雜模型時(shí)效果不佳.Gui 等［5］結(jié)合進(jìn)程代數(shù)理論對(duì)AADL 模型的組件進(jìn)行分析，但僅支持比較簡(jiǎn)單的調(diào)度模型.形式化方法能夠更精確地研究系統(tǒng)特性，AADL 屬于高層建模語(yǔ)言，需要將其轉(zhuǎn)換為較低層次的形式化模型，實(shí)現(xiàn)實(shí)時(shí)系統(tǒng)的研究與相關(guān)驗(yàn)證工具的有效結(jié)合［6-8］.AADL2BIP［9］工具能將AADL 模型轉(zhuǎn)換成BIP 語(yǔ)言，使用驗(yàn)證工具VERSA［10］對(duì)其進(jìn)行驗(yàn)證，但支持的調(diào)度類型較少.Hugues 等［11］將AADL 模型轉(zhuǎn)換成Petri 模型進(jìn)行形式化驗(yàn)證.Johnsen［12］利用UPPAAL 工具建立了時(shí)間自動(dòng)機(jī)模型，支持基本固定優(yōu)先級(jí)的調(diào)度策略模擬與驗(yàn)證.

本文借助時(shí)間自動(dòng)機(jī)(timed automata，TA)的形式化驗(yàn)證手段，通過模型轉(zhuǎn)換的方法將AADL調(diào)度模型轉(zhuǎn)換到時(shí)間自動(dòng)機(jī)模型，并利用UPPAAL 工具對(duì)原模型進(jìn)行等價(jià)驗(yàn)證.

1 模型分析與語(yǔ)義轉(zhuǎn)換

AADL 模型文件被自動(dòng)轉(zhuǎn)換插件解析后，根據(jù)語(yǔ)義規(guī)則將AADL 的元素映射成時(shí)間自動(dòng)機(jī)中對(duì)應(yīng)的元素，形成時(shí)間自動(dòng)機(jī)模型.然后，利用UPPAAL 工具對(duì)生成的時(shí)間自動(dòng)機(jī)模型進(jìn)行性質(zhì)驗(yàn)證.該方法的核心是構(gòu)建出不同調(diào)度策略的時(shí)間自動(dòng)機(jī)模型以及AADL 模型到時(shí)間自動(dòng)機(jī)模型的映射法則(見圖1).

圖1 AADL 模型可調(diào)度性驗(yàn)證方法框架

1.1 AADL 模型

AADL 調(diào)度模型定義為一個(gè)四元組S=〈R，Z，TP，Q〉.其中，R 為處理器組件，其定義的屬性集包含了處理器的特性，且調(diào)度模型中主要關(guān)注Thread-Limit(線程限制個(gè)數(shù))與Scheduling-Protocol(調(diào)度策略)兩個(gè)屬性，前者設(shè)定了綁定在一個(gè)處理器上的最大線程數(shù)量，后者則規(guī)定了處理器調(diào)度策略;Z 為進(jìn)程組件，使用Allowed-Processor-Binding(允許處理器綁定)與Actual-Processor-Binding(實(shí)際處理器綁定)來綁定處理器，且可通過屬性和子組件定義的方式，在進(jìn)程組件中定義線程子組件，并將進(jìn)程作為管理單元關(guān)聯(lián)起任務(wù)和任務(wù)的執(zhí)行單元;TP為線程集合;Q 為端口之間的連接.令ti為第i 個(gè)線程，則ti=〈x，f，p，e，m〉.其中，x∈N 為線程標(biāo)識(shí)符;f 為綁定于線程的數(shù)據(jù)端口，包含輸入端口和輸出端口;p 為與調(diào)度策略相關(guān)的屬性集合，包括線程派發(fā)策略Dispatch-Protocol、線程時(shí)鐘周期P、線程執(zhí)行時(shí)間W、約定的截止時(shí)間D 和線程的優(yōu)先級(jí)F;e 為模式狀態(tài)，主要配合行為模型定義系統(tǒng)的不同狀態(tài)集合;m 為行為模型，定義了線程的詳細(xì)動(dòng)作，是對(duì)執(zhí)行模型的擴(kuò)展.

1.2 時(shí)間自動(dòng)機(jī)模型

一個(gè)時(shí)間自動(dòng)機(jī)可以表示為一個(gè)六元組A=〈L，l0，C，V，E，I〉.其中，L 為有窮狀態(tài)集合;l0為初始狀態(tài);C 為有窮時(shí)鐘集合;V 為同步標(biāo)號(hào)(時(shí)間或指定信息)的有窮集合;E∈L ×V ×φ(C)×2C×L為轉(zhuǎn)移集合;I:L→φ(C)表示L 中的位置賦以某個(gè)時(shí)鐘約束，此時(shí)鐘約束即稱為位置不變式.

一個(gè)時(shí)間自動(dòng)機(jī)A 的語(yǔ)義可以通過與時(shí)間系統(tǒng)相關(guān)的轉(zhuǎn)移系統(tǒng)SA進(jìn)行定義，用二元組〈l，ν〉來表示，其中l(wèi)∈L 為A 的某一狀態(tài)，ν 為滿足不變式I(l)的某一時(shí)鐘解釋.若l=l0，在該初始位置上所有時(shí)鐘變量的初值為0.

SA包括2 種類型的遷移:①延遲遷移.狀態(tài)因時(shí)間流逝而發(fā)生的改變，即其中δ≥0 為實(shí)數(shù)值時(shí)間增量，ν∈I(l)，且ν + δ∈I(l).②位置遷移.狀態(tài)因位置轉(zhuǎn)移而改變，即滿足的條件，發(fā)生由狀態(tài)l 到l'的遷移，且ν∈I(l)，ν'∈I(l')，其中g(shù)，a，u 分別為守衛(wèi)條件、同步通道和更新操作的集合.

1.3 AADL 調(diào)度模型到時(shí)間自動(dòng)機(jī)模型的語(yǔ)義轉(zhuǎn)換

建立AADL 調(diào)度模型到時(shí)間自動(dòng)機(jī)的語(yǔ)義映射，將處理器組件與各個(gè)線程分別映射為一個(gè)時(shí)間自動(dòng)機(jī)，從而建立起一個(gè)調(diào)度模型的時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò).定義轉(zhuǎn)換規(guī)則Γ(A)=〈B，N，K〉.其中，B 為時(shí)間自動(dòng)機(jī)網(wǎng)絡(luò)中的自動(dòng)機(jī)集合;N={x，sch-info}為映射中全局變量，表示線程標(biāo)號(hào)和線程屬性信息;K={派發(fā)，運(yùn)行，完成，錯(cuò)誤}為全局同步通道信號(hào).

AADL 模型到時(shí)間自動(dòng)機(jī)模型的轉(zhuǎn)換映射主要包括以下2 種:

1)線程組件到時(shí)間自動(dòng)機(jī)的映射.即Bi+1=各線程分別轉(zhuǎn)換到一個(gè)時(shí)間自動(dòng)機(jī)用于表示執(zhí)行狀態(tài)的切換.其中，轉(zhuǎn)換規(guī)則ΓG:G→A 將線程的語(yǔ)義映射到時(shí)間自動(dòng)機(jī)模型語(yǔ)義.ΓG(ti)的轉(zhuǎn)換對(duì)應(yīng)ti→〈L，l0，C，V，E，I〉.其中，映射法則的語(yǔ)義已明確，需建立具體的映射法則來確定A 語(yǔ)義中的具體內(nèi)容.線程的基本狀態(tài)映射為A 的初始化、就緒、執(zhí)行、出錯(cuò)和被搶占5個(gè)狀態(tài)，即L={初始化，準(zhǔn)備，運(yùn)行，錯(cuò)誤，搶占}.此時(shí)，C={k}為控制線程派發(fā)和記錄線程截止時(shí)間的時(shí)鐘;V={P，W，D，F(xiàn)}用于記錄時(shí)鐘周期P、執(zhí)行時(shí)間W、截止時(shí)間D 和優(yōu)先級(jí)的整型變量F.E={初始→準(zhǔn)備，準(zhǔn)備→運(yùn)行，運(yùn)行→初始化，初始→準(zhǔn)備，運(yùn)行→錯(cuò)誤，g，a，u}為不同狀態(tài)之間的轉(zhuǎn)移;I(l0)={k≤P}.這里僅給出了周期線程在初始狀態(tài)上的不變條件，對(duì)于非周期線程，狀態(tài)轉(zhuǎn)移由同步通道觸發(fā).

2)處理器組件到時(shí)間自動(dòng)機(jī)的映射.即B0=ΓR(R)，ΓR(R):R→A，將處理器組件及調(diào)度相關(guān)模型映射到一個(gè)時(shí)間自動(dòng)機(jī).轉(zhuǎn)換的規(guī)則為ΓR(R)=〈L，l0，C，V，E，I〉.此處，L={等待，調(diào)度器，運(yùn)行，搶占，完成，死鎖};l0= {等待};C= {sch-clocks［x］，switch-clock}，V={t，x，T，o，s}，其中s 為切換時(shí)間，t 為當(dāng)前獲得執(zhí)行權(quán)限的線程，o為被搶占線程的個(gè)數(shù).

2 AADL 調(diào)度模型時(shí)間自動(dòng)機(jī)設(shè)計(jì)

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

根據(jù)AADL 中線程自動(dòng)機(jī)的情況，設(shè)計(jì)了非可搶占調(diào)度策略下周期線程的時(shí)間自動(dòng)機(jī)模板(見圖2).由圖可知，當(dāng)局部時(shí)鐘k 達(dá)到周期時(shí)間P 后，線程從初始狀態(tài)轉(zhuǎn)移到準(zhǔn)備狀態(tài)，并產(chǎn)生派發(fā)信號(hào)dispatch［x］!，并且將線程信息賦值給全局變量.sch-info［x］［0］存儲(chǔ)線程的最大執(zhí)行時(shí)間Wmax，sch-info［x］［1］存入了線程的優(yōu)先級(jí)F.線程自動(dòng)機(jī)接受調(diào)度器的同步信號(hào)決定了運(yùn)行和初始狀態(tài)的轉(zhuǎn)移.當(dāng)局部時(shí)鐘k 超過線程規(guī)定的截止時(shí)間D 時(shí)，自動(dòng)機(jī)進(jìn)入錯(cuò)誤狀態(tài)，并通過錯(cuò)誤通道將錯(cuò)誤信號(hào)發(fā)送給調(diào)度器模板.

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

根據(jù)非可搶占調(diào)度策略的調(diào)度規(guī)則，設(shè)計(jì)了相應(yīng)的調(diào)度器模板(見圖3).由圖可知，初始狀態(tài)為等待狀態(tài)，調(diào)度器Ⅰ和完成是2 種限制狀態(tài)，在該狀態(tài)下不發(fā)生時(shí)間流逝.在狀態(tài)轉(zhuǎn)移中，分別處理在不同狀態(tài)下接收到線程派發(fā)信號(hào)后調(diào)度器對(duì)新派發(fā)線程的處理.調(diào)度器維護(hù)了一個(gè)線程的等待隊(duì)列ready-q，新派發(fā)的線程dispatch［x］首先進(jìn)入該隊(duì)列并按照優(yōu)先級(jí)計(jì)算策略進(jìn)行排序，此處T 表示當(dāng)前派發(fā)線程的個(gè)數(shù)，在非可搶占調(diào)度策略下，線程一旦進(jìn)入運(yùn)行狀態(tài)，在執(zhí)行結(jié)束之前是不能進(jìn)行中斷的，并通過completion 函數(shù)對(duì)ready-q 進(jìn)行維護(hù).若系統(tǒng)中的任何一個(gè)線程超時(shí)而進(jìn)入錯(cuò)誤狀態(tài)，調(diào)度器時(shí)間自動(dòng)機(jī)通過錯(cuò)誤廣播通道接收到錯(cuò)誤信號(hào)后進(jìn)入死鎖狀態(tài)，自動(dòng)機(jī)停止執(zhí)行.

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

在AADL 模型中，處理器組件的屬性Thread-Swap-Execution-Time 規(guī)定了線程切換的時(shí)間開銷.為了實(shí)現(xiàn)這種轉(zhuǎn)換，擴(kuò)展了非可搶占調(diào)度策略下調(diào)度器的模板，設(shè)計(jì)了帶有線程切換時(shí)間的非可搶占調(diào)度器模板(見圖4).模板擴(kuò)充定義了切換時(shí)鐘switch-clock 和設(shè)置切換時(shí)間s，去掉調(diào)度器Ⅰ狀態(tài)的限制屬性，增加switch-clock ＜=s 的不變條件，以實(shí)現(xiàn)線程狀態(tài)在時(shí)間切換時(shí)的模擬，并對(duì)該狀態(tài)的轉(zhuǎn)出條件和通向死鎖狀態(tài)的路徑進(jìn)行了相應(yīng)調(diào)整.

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

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

與非可搶占調(diào)度策略相比，可搶占調(diào)度策略下周期線程的時(shí)間自動(dòng)機(jī)模板增加了一個(gè)被搶占狀態(tài).當(dāng)運(yùn)行狀態(tài)線程的運(yùn)行權(quán)限被更高優(yōu)先級(jí)的線程搶占后，該自動(dòng)機(jī)進(jìn)入搶占狀態(tài)，待優(yōu)先級(jí)高的線程執(zhí)行完畢，被搶占的線程恢復(fù)執(zhí)行，返回運(yùn)行狀態(tài).在該狀態(tài)下，執(zhí)行時(shí)鐘不增長(zhǎng)，截止時(shí)鐘持續(xù)增長(zhǎng).線程的搶占加大了恢復(fù)調(diào)度器模板的復(fù)雜程度，相對(duì)于非可搶占調(diào)度器的模板，狀態(tài)集合增加了調(diào)度狀態(tài)Ⅱ和搶占狀態(tài)2 個(gè)狀態(tài).在運(yùn)行狀態(tài)下，當(dāng)有新的線程派發(fā)時(shí)，調(diào)度器轉(zhuǎn)移到調(diào)度器Ⅱ狀態(tài)，判斷新派發(fā)線程的優(yōu)先級(jí).在該時(shí)間自動(dòng)機(jī)模板中，引入了被搶占線程棧preempt-stack［z］［2］，記錄了被搶占線程的標(biāo)號(hào)和被搶占時(shí)間，位于棧頂?shù)脑鼐哂凶罡叩膬?yōu)先級(jí).

在UPPAAL 工具中，時(shí)鐘參數(shù)的初始值為0或?yàn)橐粋€(gè)比較結(jié)果(當(dāng)前時(shí)鐘參數(shù)與固定整數(shù)的差值).基于這一限制，對(duì)可搶占調(diào)度器模板中被搶占時(shí)間的計(jì)算方法進(jìn)行設(shè)計(jì).定義指定線程t 的執(zhí)行時(shí)間為Wt，截止時(shí)間為Dt，時(shí)間自動(dòng)機(jī)中的運(yùn)行時(shí)鐘為ct，截止時(shí)鐘為dt，恢復(fù)時(shí)的被搶占時(shí)間為Pt，已派發(fā)線程的優(yōu)先級(jí)高于線程t 個(gè)數(shù)為n，則有

假設(shè)存在3 個(gè)線程t1，t2，t3，優(yōu)先級(jí)滿足Priority(t1)＜Priority(t2)＜Priority(t3).如圖5所示，在點(diǎn)X 處線程t1產(chǎn)生派發(fā)，運(yùn)行時(shí)鐘ct1和截止時(shí)鐘dt1都被置為0，此時(shí)隊(duì)列中t1的優(yōu)先級(jí)最高，故被搶占時(shí)間Pt1=0;在點(diǎn)Y 處，更高優(yōu)先級(jí)的t2派發(fā)，t1需要等待t2線程執(zhí)行完畢后才能恢復(fù)執(zhí)行，則t1的搶占時(shí)間Pt1等于t2的執(zhí)行時(shí)間Wt2與t1已有的搶占時(shí)間之和;當(dāng)更高優(yōu)先級(jí)的線程t3在點(diǎn)H 處被派發(fā)時(shí)，則t1的搶占時(shí)間等于t3的執(zhí)行時(shí)間與t1已有的搶占時(shí)間之和.在點(diǎn)O 處，判斷條件ct1≥Wt1+Pt1判斷了t1除去被搶占時(shí)間實(shí)際運(yùn)行的時(shí)間是否大于或等于t1的執(zhí)行時(shí)間Wt1，若滿足，則t1執(zhí)行完畢.判斷條件dt1≥Dt1判斷t1的執(zhí)行是否超過了規(guī)定的截止時(shí)間.

圖5 線程搶占執(zhí)行示意圖

若計(jì)入線程切換的時(shí)間，則

式(2)中，由于一次搶占帶來2 次線程的切換，故在線程恢復(fù)時(shí)共進(jìn)行了2n 次的線程切換.

2.3 可調(diào)度性驗(yàn)證語(yǔ)句

UPPAAL 驗(yàn)證器中利用時(shí)序邏輯TCTL 可以驗(yàn)證一些基本性質(zhì)，如線程死鎖.對(duì)于調(diào)度模型的可調(diào)度性驗(yàn)證，所使用的部分性質(zhì)驗(yàn)證語(yǔ)句見表1.

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

3 自動(dòng)化模型轉(zhuǎn)換插件的功能

本文基于AADL 建模工具OSATE 設(shè)計(jì)開發(fā)了自動(dòng)化模型轉(zhuǎn)換的插件AadlToUpaalL Convert Plug-in，并將其嵌入到OSTATE 工具中，形成了AADL 模型的建模、轉(zhuǎn)換、驗(yàn)證與分析的集成開發(fā)環(huán)境.自動(dòng)模型轉(zhuǎn)換插件實(shí)現(xiàn)了如下三大功能:①AADL 模型解析.即負(fù)責(zé)讀取建模工具中建立的AADL 模型，按照語(yǔ)義信息與格式規(guī)范，解析AADL 模型在轉(zhuǎn)換中所需的基本信息，構(gòu)建在插件程序中AADL 的對(duì)象模型.②模型轉(zhuǎn)換.即根據(jù)文本建立的模型轉(zhuǎn)換規(guī)則，將讀入的AADL 模型信息對(duì)應(yīng)映射為時(shí)間自動(dòng)的基本元素，構(gòu)建時(shí)間自動(dòng)機(jī)的對(duì)象模型.③時(shí)間自動(dòng)機(jī)模型生成.即解析文件格式，并將得到的時(shí)間自動(dòng)機(jī)對(duì)象模型轉(zhuǎn)換為模型文件，實(shí)現(xiàn)了模型自動(dòng)構(gòu)建的功能.由于時(shí)間自動(dòng)機(jī)在UPPAAL 工具中以狀態(tài)圖的形式展示，文件中也保存了圖形的基本信息，故目標(biāo)文件生成模塊還需要調(diào)整模型文件中狀態(tài)和邊的坐標(biāo)信息.

圖6 自動(dòng)化管焊系統(tǒng)焊槍速度控制模塊AADL 模型結(jié)構(gòu)

4 系統(tǒng)測(cè)試

4.1 實(shí)例測(cè)試

本文以自動(dòng)化管焊設(shè)備焊槍速度控制系統(tǒng)為例，建立了系統(tǒng)的AADL 模型，該模型由系統(tǒng)組件(WeldingSystem)、處理器組件(Processor1)、進(jìn)程組件(Process1)、線程組件(CalThread，Th1，Th2)、設(shè)備組件(Sensor1，SpeedActuator)和若干端口、連接組成.其功能是通過一個(gè)傳感器采集到焊槍槍頭電機(jī)的轉(zhuǎn)速信息并傳遞給計(jì)算線程，由計(jì)算線程處理后產(chǎn)生控制信號(hào)傳遞給控制設(shè)備，從而形成一個(gè)速度調(diào)節(jié)反饋的系統(tǒng).該模型結(jié)構(gòu)如圖6所示.

在OSATE 工具中，建立含有3 個(gè)周期線程的AADL 系統(tǒng)模型.語(yǔ)法驗(yàn)證通過后，實(shí)例化系統(tǒng)得到AAXL 類型的系統(tǒng)模型文件.利用模型轉(zhuǎn)換插件對(duì)模型進(jìn)行自動(dòng)轉(zhuǎn)換后，在UPPAAL 工具中模擬系統(tǒng)的狀態(tài)轉(zhuǎn)移，在驗(yàn)證器中利用自動(dòng)生成的性質(zhì)查詢語(yǔ)句驗(yàn)證系統(tǒng)的時(shí)間特性.經(jīng)測(cè)試，系統(tǒng)不發(fā)生死鎖且Exist ＜＞Processor.MissedDeadline 性質(zhì)不滿足.

4.2 性能分析

本文設(shè)計(jì)了一組包含20 個(gè)線程的測(cè)試用例，每個(gè)線程的周期和截止時(shí)間均為20 ms，執(zhí)行時(shí)間均為1 ms，線程的優(yōu)先級(jí)按照數(shù)字序號(hào)依次設(shè)定為0 ～19.根據(jù)Liu 等［13］針對(duì)RMS 調(diào)度策略提出的使用率限定定理，理論上確定該組任務(wù)的所有子集都是可調(diào)度的.可調(diào)度的任務(wù)集合對(duì)應(yīng)的時(shí)間自動(dòng)機(jī)性質(zhì)的驗(yàn)證需要遍歷整個(gè)狀態(tài)空間，耗時(shí)較長(zhǎng).性質(zhì)驗(yàn)證計(jì)算過程中，UPPAAL 服務(wù)進(jìn)程的CPU 利用率穩(wěn)定在25%左右，內(nèi)存消耗隨著驗(yàn)證的推進(jìn)而不斷增長(zhǎng)，驗(yàn)證時(shí)間和內(nèi)存使用的趨勢(shì)圖分別見圖7和圖8.

圖7 驗(yàn)證耗時(shí)隨周期線程數(shù)變化圖

圖8 驗(yàn)證內(nèi)存消耗隨周期線程數(shù)變化圖

5 結(jié)語(yǔ)

利用時(shí)間自動(dòng)機(jī)形式化驗(yàn)證手段，研究了AADL 模型中調(diào)度模型到時(shí)間自動(dòng)機(jī)模型的轉(zhuǎn)換方法.設(shè)計(jì)了非可搶占與可搶占策略下的時(shí)間自動(dòng)機(jī)模板以及AADL 模型元素到時(shí)間自動(dòng)機(jī)模板的轉(zhuǎn)換法則.利用UPPAAL 與時(shí)間自動(dòng)機(jī)模型來驗(yàn)證AADL 所描述系統(tǒng)的可調(diào)度性.下一步的研究主要集中于擴(kuò)展所設(shè)計(jì)的時(shí)間自動(dòng)機(jī)以及模型轉(zhuǎn)換法則，使其支持更多的調(diào)度策略以及更復(fù)雜的AADL 模型表述.

References)

［1］ Kleppe A G，Warmer J B，Bast W.MDA explained:the model driven architecture:practice and promise［M］.Boston，USA:Addison-Wesley Professional，2003:1-20.

［2］ Peled D A.Software reliability methods ［M］.New York，USA:Springer Science ＆ Business Media，2013:100-125.

［3］ Singhoff F，Legrand J，Nana L，et al.Scheduling and memory requirements analysis with AADL［C］//Proceedings of the 2005 Annual ACM SIGAda International Conference on Ada.Atlanta，GA，USA，2005:1-10.

［4］ Singhoff F，Plantec A，Dissaux P，et al.Investigating the usability of real-time scheduling theory with the Cheddar project［J］.Real-Time Systems，2009，43(3):259-295.

［5］ Gui S，Luo L，Li Y，et al.Formal schedulability analysis and simulation for AADL［C］//ICESS'08 International Conference on Embedded Software and Systems.Chengdu，China，2008:429-435.

［6］ Abdoul T，Champeau J，Dhaussy P T，et al.AADL execution semantics transformation for formal verification［C］//13th IEEE International Conference on Engineering of Complex Computer Systems.Belfast，Northern Ireland，2008:263-268.

［7］ Hu K，Zhang T，Yang Z，et al.Exploring AADL verification tool through model transformation［J］.Journal of Systems Architecture，2015，61(3/4):141-156.

［8］ 符寧，杜承烈，李建良，等.AADL 分級(jí)調(diào)度模型的分析與驗(yàn)證［J］.計(jì)算機(jī)研究與發(fā)展，2015，52(1):167-176.Fu Ning，Du Chenglie，Li Jianliang，et al.Analysis and verification of AADL hierarchical schedulers［J］.Journal of Computer Research and Development，2015，52(1):167-176.(in Chinese)

［9］ Chkouri M Y，Robert A，Bozga M，et al.Translating AADL into BIP-application to the verification of realtime systems［M］//Models in Software Engineering，Berlin，Germany:Springer，2009:5-19.

［10］ Clarke D，Lee I，Xie H L.VERSA:a tool for the specification and analysis of resource-bound real-time systems，MS-CIS-93-77 ［R］.Philadelphia，PA，USA:Department of Computer and Information Science，University of Pennsylvania，1993.

［11］ Hugues J，Zalila B，Pautet L，et al.From the prototype to the final embedded system using the Ocarina AADL tool suite［J］.ACM Transactions on Embedded Computing Systems (TECS)，2008，7(4):42-1-42-25.

［12］ Johnsen A.Architecture-based verification of dependable embedded systems ［D］.V?ster?s， Sweden:M?lardalen University，2013.

［13］ Liu C L，Layland J W.Scheduling algorithms for multiprogramming in a hard-real-time environment［J］.Journal of the ACM (JACM)，1973，20(1):46-61.