基于Uppaal的多處理器實(shí)時(shí)系統(tǒng)的可調(diào)度性分析.pdf

1、相較于單處理器的執(zhí)行平臺(tái)，多處理器的執(zhí)行平臺(tái)由于可以提供更強(qiáng)大的處理能力而正在被越來越廣泛的應(yīng)用到各類實(shí)時(shí)系統(tǒng)中。例如，越來越多的嵌入式系統(tǒng)使用多處理器的平臺(tái)來執(zhí)行實(shí)時(shí)的應(yīng)用程序，而這些應(yīng)用程序又被分割為一個(gè)個(gè)的實(shí)時(shí)任務(wù)在平臺(tái)上執(zhí)行。又如，在有些系統(tǒng)上，實(shí)時(shí)的任務(wù)在系統(tǒng)運(yùn)行時(shí)生成，繼而在有時(shí)間限制的條件下被執(zhí)行，如一系列由事件觸發(fā)的中斷需要在它們的截止時(shí)間內(nèi)可搶占的執(zhí)行。
　　多處理器的實(shí)時(shí)系統(tǒng)的設(shè)計(jì)是一件十分復(fù)雜工作，需要考慮眾

2、多的因素，如處理器的數(shù)目，處理器的類型和結(jié)構(gòu)，任務(wù)的分配，操作系統(tǒng)的選擇等等。由于在系統(tǒng)設(shè)計(jì)時(shí)各部分的選擇（如以上提及的選擇）具有一定的自由性，要設(shè)計(jì)一個(gè)正確的，有效的系統(tǒng)就成了一項(xiàng)不小的挑戰(zhàn)。這需要設(shè)計(jì)者對(duì)各部分如何獨(dú)立運(yùn)作以及它們之間如何協(xié)同運(yùn)作都要精心設(shè)計(jì)，這通常通過對(duì)系統(tǒng)進(jìn)行建模來實(shí)現(xiàn)，而建模之后往往要對(duì)系統(tǒng)的正確性和有效性進(jìn)行驗(yàn)證，由于各個(gè)系統(tǒng)的運(yùn)行機(jī)制各不相同，要驗(yàn)證的系統(tǒng)屬性常常不一樣，但有一個(gè)重要的問題往往在系統(tǒng)設(shè)計(jì)時(shí)就

3、需要解決，那就是確保系統(tǒng)中的任務(wù)能在它們的截止時(shí)間內(nèi)執(zhí)行完畢，這就是所謂的可調(diào)度性分析。
　　目前存在著一些解決實(shí)時(shí)系統(tǒng)的可調(diào)度性分析問題的方法，如傳統(tǒng)的可調(diào)度性測(cè)試方法，它基于處理器的利用上界（processor utilization bounds)，如果測(cè)試值低于上界，則系統(tǒng)可調(diào)度，如果高于上界，則無法判斷。任務(wù)自動(dòng)機(jī)（task automata）是一類擴(kuò)展了的時(shí)間自動(dòng)機(jī)，它被專門用來進(jìn)行可調(diào)度性分析。Times是一個(gè)基于任

4、務(wù)自動(dòng)機(jī)理論的工具，這個(gè)工具被用來在單處理器平臺(tái)上面進(jìn)行可調(diào)度性分析。
　　盡管實(shí)時(shí)系統(tǒng)的可調(diào)度性分析已經(jīng)有了眾多方法，但是，目前沒有一種通用且有效的方法適用于多處理器平臺(tái)，也沒有一種方法將系統(tǒng)的各個(gè)部分完整的指定，分層次的建模，并且整體的看待系統(tǒng)的可調(diào)度性分析和形式化驗(yàn)證。在這樣的背景下，如何在時(shí)間自動(dòng)機(jī)理論的基礎(chǔ)上提出一種系統(tǒng)模型，這個(gè)模型能支持多處理器平臺(tái)上的形式化的驗(yàn)證和模擬，并且支持系統(tǒng)的正確性分析，如可調(diào)度性，就是一個(gè)

5、值得我們研究的問題。
　　在這篇文章里，我們首先將一個(gè)典型的實(shí)時(shí)系統(tǒng)劃分成以下幾個(gè)模塊：硬件環(huán)境，任務(wù)系統(tǒng)和多處理器的執(zhí)行平臺(tái)，然后，我們?cè)谀Ｐ托ｒ?yàn)工具Uppaal中用時(shí)間自動(dòng)機(jī)對(duì)各個(gè)模塊建模，用以刻畫它們獨(dú)立和交互的行為，這樣，我們可以在一個(gè)統(tǒng)一的框架當(dāng)中對(duì)系統(tǒng)進(jìn)行形式化驗(yàn)證和可調(diào)度性分析。同時(shí)，我們?cè)谔岢龅哪Ｐ椭辛粝铝丝晒┰O(shè)計(jì)者修改的接口，使得此模型具有一定的通用性和可伸縮性，設(shè)計(jì)者們可以根據(jù)現(xiàn)實(shí)的實(shí)時(shí)系統(tǒng)進(jìn)行修改，以適應(yīng)系統(tǒng)