摘 要：基于成分分析的層次化調度框架，其中使用到Uppaal，這是一種集成的工具環(huán)境，被用來對被轉換時間自動機網絡模型的實時系統(tǒng)進行建模、校驗和驗證。它是由瑞典Uppsala大學的信息技術學院和丹麥Aalborg大學的計算科學學院聯(lián)合開發(fā)的。主要討論了一種可重構的調度框架，表示層次化結構，調度策略，具體任務行為和可共享資源均可重構。

關鍵詞：層次化結構；可重構；調度策略

中圖分類號：TP391.41

基于成分分析的層次化調度框架，其中使用到Uppaal，表示層次化結構，調度策略，具體任務行為和可共享資源均可重構。每一階段的搶占任務的行為被指定為定時動作列表，作為組成該框架的可參數(shù)化的自動定時裝置的某個輸入。構件可能有不同的調度策略，每一個構件使用UPPAAL獨立分析。該框架已被應用于某個航空設置系統(tǒng)的調度分析。

該論文的主要貢獻為：

—一種組合分析方法，適用于可調度性依賴于它的子系統(tǒng)的遞歸調度能力的系統(tǒng)。

—一種重構調度框架，適用于可以實例化為不同的配置來滿足不同的應用的系統(tǒng)結構。

——具體任務行為模型，適用于需要CPU和資源的定時動作序列

與非實時系統(tǒng)相比，嵌入式實時系統(tǒng)因其所控制物理過程的動態(tài)性，要求運行于其中的單個任務必須滿足其時限要求，以確保整個系統(tǒng)的正確性和安全性[1]。在航空航天、電信、制造、國防等領域，對實時系統(tǒng)有著強烈的應用需求。實時處理和實時系統(tǒng)的研究和應用工作已經有了相當長的歷史，在實時任務調度理論、實時操作系統(tǒng)、實時通信等方面取得了大量成果。

實時任務調度理論是實時處理技術的核心和關鍵。這是因為，實時任務具有時限要求，在一個或多個處理器之間調度實時任務，需要判斷是否每個任務的執(zhí)行都能在其截止期限內完成。如果每個任務的執(zhí)行都能在其截止期限內完成，則稱該調度是可行?？烧{度性判定就是判定給定的n個實時任務在應用某種調度算法的前提下能否產生一個可行的調度。調度算法的設計要盡可能滿足任務可調度性的要求。

事實上，該框架是通過使用可參數(shù)化的定時自動裝置模型實現(xiàn)。

層次化的可調度系統(tǒng)包括了有限的部件集，一種調度策略和（全局）資源。相應的，每個構件使用有限實體集的并行結構來完成其分配的工作量，此處實體集是指任務集或者是使用同種調度策略的構件，可以看出我們并沒有考慮到構件的本地資源。系統(tǒng)任務是帶有不同輸入參數(shù)的定時自動裝置的實例，該任務模型的特別參數(shù)是定時動作的列表，它給出了給定任務的具體行為。這份列表包括了抽象計算步驟，鎖定和解鎖資源。正是由于可參數(shù)化，該框架可以很容易的使每個明確的層次化調度應用實例化。相似的，每個調度策略可以被分別模擬并使每個構件實例化。

一個層次化調度系統(tǒng)包括了大量的層次化結構的調度系統(tǒng)，可以展示為一個擁有節(jié)點的樹，這個系統(tǒng)的每一個節(jié)點都擁有一個調度器來調度它的孩子構件。

該結構將系統(tǒng)模型作為一系列層次化的構件來架構。相應的，每個構件是實體集以及本地調度器和本地資源的并行結構。一個父親構件將它每個孩子構件的實時接口作為給定實時接口的單個任務。該構件根據(jù)它的孩子的實時接口分配資源。也就是說，每個構件均可以通過時間、預算、調度策略來參數(shù)化，其中，預算指出了在父親層計算機應該提供給該構件的執(zhí)行時間，調度策略指出了該構件提供給孩子實體的資源分配。對該構件（調度單元）的分析包括根據(jù)構件調度策略檢查孩子實體在預算內是否可以被調度。一個構件也可以通過作為服務構件本地資源的一系列典型資源參數(shù)化。以下為參數(shù)符號及概念：

Ti第i個實時任務；n任務集合中任務的數(shù)量；ei任務Ti的執(zhí)行時間；Pi任務Ti的周期；t系統(tǒng)運行的時間，t≥0；ri任務Ti的釋放時間；di任務Ti的相對時間限（相對于釋放時間）；Di任務Ti的絕對時間限。任務的釋放時間是指所有用來開始執(zhí)行任務的資源都可用的時間，即任務開始執(zhí)行的時間。任務的絕對時間限是指任務必須完成的時間。任務的相對時間限是指絕對時間限減去釋放時間。

不確定性模型的其實是一個數(shù)據(jù)源分配模型，它為系統(tǒng)提供執(zhí)行需要的原始數(shù)據(jù)。這種基于結構的調度模型是為任務分配數(shù)據(jù)，因此在任務執(zhí)行過程中，如何在正確的時間的讀入數(shù)據(jù)，直接影響了程序的執(zhí)行效率。如果數(shù)據(jù)的讀入在程序的執(zhí)行過程中總是出現(xiàn)數(shù)據(jù)漏讀的情況，總是在等待數(shù)據(jù)讀入，那么將會極大的降低程序的效率，程序的執(zhí)行過程中將會有很多垃圾時間。而不確定供應商模型就給了這樣一種合理的、動態(tài)的分配模型，使得程序在執(zhí)行過程不會出現(xiàn)斷層。

我們現(xiàn)在可以為這個分層實時系統(tǒng)的建模和可調度性分析定義一個組成框架。這個框架可以作為我們運用UPPAAL和UPPAAL SMC來分析時間自動裝置的一個可重用的例子。當建立一個分層調度應用模型的時候，這個可重用的模型可以確保具體的工作行為和需要系統(tǒng)工程師來規(guī)范的分層結構。這個框架也使得在每個分層的層次中的調度變化及時操作。對比我們基本的建模方法去分析這個建模，我們的框架工作使得我們這個模型更加具有競爭性，也更加的實用。我們已經成功應用我們的組成框架來建立一個航空電子設備系統(tǒng)，而且分析了它的可調度性。在未來的工作中，我們喜劇學習怎么樣以一個自動化的方式去判斷最佳時間的資源要求。我們也計劃考慮多核平臺的能量效率問題。

參考文獻：

[1]Boudjadar，A.Hierarchical Scheduling Framework Based on Compositional Analysis Using Uppaal，in Formal Aspects of Component Software，J.L.Fiadeiro，Z.Liu，and J.Xue，Editors.Springer International Publishing，2014.

[2]Mikucionis，M.Schedulability Analysis Using Uppaal：Herschel-Planck Case Study，in Leveraging Applications of Formal Methods，Verification，and Validation，Pt Ii，T.Margaria and B. Steffen，Editors，2010：175-190.

[3]Moonzoo Kim，Yunho Kim.Hotae Kim\"A Comparative Study of Software Model Checkers as Unit Testing Tools：An Industrial Case Study\"，Software Engineering，IEEE Transactions on，2011（02）：146-160.

作者簡介：張夢琪，2011級軟件工程學生，參加2014年網易“中國合伙人”軟件開發(fā)大賽進入決賽，并與暑期參與新加坡國立大學計算機學院交流營活動。在校期間連續(xù)兩年獲得“優(yōu)秀學生”稱號，并榮獲“優(yōu)秀畢業(yè)生”稱號。

作者單位：四川大學軟件學院，成都 610000