基于模型檢測(cè)的多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性自動(dòng)化分析

杜伊

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都 610065)

基于模型檢測(cè)的多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性自動(dòng)化分析

杜伊

（四川大學(xué)計(jì)算機(jī)學(xué)院，成都 610065)

近年來，模型檢測(cè)技術(shù)獲得快速的發(fā)展，已有學(xué)者將模型檢測(cè)技術(shù)用于多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性分析。但如果對(duì)每個(gè)實(shí)際系統(tǒng)都手工建立模型進(jìn)行可調(diào)度性驗(yàn)證，過程繁瑣且模型不可重復(fù)利用。針對(duì)此，開發(fā)一個(gè)工具用于自動(dòng)完成可調(diào)度性檢測(cè)，并可視化顯示結(jié)果。

模型檢測(cè)技術(shù)；多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性；自動(dòng)化；可視化

0 引言

模型檢測(cè)[1]是一種形式化驗(yàn)證方法，通過自動(dòng)地窮盡搜索待驗(yàn)證系統(tǒng)的狀態(tài)空間，驗(yàn)證系統(tǒng)是否滿足給定的性質(zhì)，并在系統(tǒng)不滿足性質(zhì)時(shí)給出違背性質(zhì)的反例。

如果一個(gè)實(shí)時(shí)任務(wù)的響應(yīng)時(shí)間小于或等于它的截止時(shí)間，我們稱這個(gè)任務(wù)是可調(diào)度的。可調(diào)度性分析[2]就是驗(yàn)證給定的系統(tǒng)環(huán)境中所有的任務(wù)是否都可調(diào)度的一種重要方法。

已有學(xué)者[3]將概率模型檢測(cè)用于多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性分析，但這一過程需要手動(dòng)建立模型，且模型不可重復(fù)利用，對(duì)不同的多處理器實(shí)時(shí)系統(tǒng)需要手動(dòng)改變模型以達(dá)到驗(yàn)證的目的。同時(shí)，現(xiàn)有的模型檢測(cè)工具和技術(shù)都要求使用者了解形式化的語言，才能對(duì)驗(yàn)證系統(tǒng)進(jìn)行描述，建模困難問題給模型檢測(cè)的廣泛應(yīng)用帶來一定阻礙。

基于此，本文開發(fā)了一個(gè)工具，實(shí)現(xiàn)可調(diào)度性分析驗(yàn)證流程的自動(dòng)化，提供配置系統(tǒng)和任務(wù)的接口，將描述的系統(tǒng)設(shè)計(jì)建立成模型檢測(cè)工具UPPAAL[4]的驗(yàn)證模型，并自動(dòng)執(zhí)行檢測(cè)過程，獲得驗(yàn)證結(jié)果后進(jìn)行進(jìn)一步分析，若生成反例則將反例有效信息提取出來形成任務(wù)調(diào)度的時(shí)序圖，通過提供的輸出接口向用戶展示分析后的可視化結(jié)果。

1 系統(tǒng)問題-模型對(duì)應(yīng)關(guān)系

多處理器實(shí)時(shí)系統(tǒng)由實(shí)時(shí)任務(wù)、運(yùn)行平臺(tái)以及任務(wù)調(diào)度模塊組成，其中，實(shí)時(shí)任務(wù)包含一組周期性任務(wù)以及任務(wù)之間的依賴關(guān)系，系統(tǒng)運(yùn)行平臺(tái)包括多個(gè)處理器和連接處理器的總線，任務(wù)調(diào)度管理模塊即系統(tǒng)維護(hù)的調(diào)度策略和調(diào)度序列等。對(duì)于實(shí)時(shí)任務(wù)調(diào)度問題中的每個(gè)部分，使用UPPAAL模型中的模型或數(shù)據(jù)結(jié)構(gòu)來建模表示，問題與模型的對(duì)應(yīng)關(guān)系如圖1所示。

圖1 問題-模型對(duì)應(yīng)關(guān)系圖

任務(wù)模板為Task，根據(jù)系統(tǒng)實(shí)際情況可以使用具體的參數(shù)(任務(wù)屬性)實(shí)例化多個(gè)任務(wù)；依賴管理器為DenpendencyManager，處理任務(wù)間的依賴關(guān)系，總線模板為Bus，處理器被抽象為一個(gè)數(shù)組，并作為調(diào)度器的參數(shù)可以根據(jù)實(shí)際系統(tǒng)進(jìn)行配置具體的值；調(diào)度管理模塊抽像為調(diào)度器模板Scheduler和策略模板Policy，支持多種策略模板，通過Scheduler實(shí)現(xiàn)處理器和調(diào)度策略的關(guān)聯(lián)，將處理器和調(diào)度策略分開建模的好處是可以更方便地?cái)U(kuò)展調(diào)度策略。

2 自動(dòng)化工具設(shè)計(jì)

2.1 需求分析

基于模型檢測(cè)的多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性自動(dòng)化分析工具實(shí)現(xiàn)了系統(tǒng)模型配置、驗(yàn)證和結(jié)果解釋的過程，預(yù)先構(gòu)造出了可配置的模型，用工具原型實(shí)現(xiàn)自動(dòng)化的模板配置，生成UPPAAL驗(yàn)證需要的模型文件.xml和性質(zhì)文件.q，調(diào)用UPPAAL的驗(yàn)證模塊進(jìn)行驗(yàn)證，并對(duì)UPPAAL給出的驗(yàn)證結(jié)果進(jìn)行解釋，再可視化反饋。這樣，用戶只需給出系統(tǒng)的屬性就能自動(dòng)地獲得可調(diào)度性分析的驗(yàn)證結(jié)果，使用過程更簡單便捷，結(jié)果反饋更直觀。此外，在工具中用戶可以保存系統(tǒng)描述信息和載入已有的系統(tǒng)描述信息。系統(tǒng)可調(diào)度自動(dòng)化分析工具的用例設(shè)計(jì)如圖2所示：

圖2 工具的用例圖

系統(tǒng)可調(diào)度性自動(dòng)化分析工具活動(dòng)圖如下：

圖3 工具的活動(dòng)圖

用戶輸入描述系統(tǒng)信息界面：輸入是詳細(xì)的系統(tǒng)描述信息，包括任務(wù)屬性、任務(wù)依賴關(guān)系、處理器屬性、總線屬性等信息，可以是用戶手動(dòng)輸入的內(nèi)容，也可以是直接打開的可擴(kuò)展名為.data的文件，若該系統(tǒng)可調(diào)度，那么輸出只有一項(xiàng)，即結(jié)果文件Model.result，并告知用戶系統(tǒng)是可調(diào)度的；若該系統(tǒng)不可調(diào)度，則輸出有兩項(xiàng)：結(jié)果文件Model.result和反例路徑Model.trace，并可視化的顯示任務(wù)調(diào)度時(shí)序圖。

2.2 詳細(xì)設(shè)計(jì)

開發(fā)環(huán)境：

●CPU：AMD AthlonII X4 640 3.0GHz

●RAM：3.0G

●操作系統(tǒng)：Microsoft Windows 8

●模型檢測(cè)工具：UPPAAL 4.1.18

●開發(fā)工具：Python-2.7，Pyqt4

嵌入式系統(tǒng)實(shí)時(shí)任務(wù)可調(diào)度性分析子系統(tǒng)設(shè)計(jì)結(jié)構(gòu)如圖4所示，組件設(shè)計(jì)如圖5所示：

圖4 工具整體設(shè)計(jì)結(jié)構(gòu)圖

圖5 工具組件設(shè)計(jì)圖

工具各個(gè)功能模塊各自具有如下功能和組件：

（1）圖形用戶界面：接收用戶輸入，反饋驗(yàn)證結(jié)果主要包含以下三個(gè)文件：

●ScheduleWindow.py主要負(fù)責(zé)用戶輸入系統(tǒng)信息界面的顯示；

●ScheduleModelResultWindow.py主要負(fù)責(zé)建立好的模型文件的顯示；

●ScheduleAnalysisResultWindow.py主要負(fù)責(zé)可調(diào)度性驗(yàn)證結(jié)果的顯示。

（3）模型配置模塊：將輸入分析模塊分析出的系統(tǒng)屬性具體數(shù)據(jù)寫入到待配置的模型中，根據(jù)具體的數(shù)值配置模型并實(shí)例化，寫入模型文件model.xml中，并將性質(zhì)寫入model.q文件中，定義ModelGenerate.py來完成這一操作。

（4）模型驗(yàn)證模塊：定義一個(gè)Controller.py文件來完成，功能是調(diào)用UPPAAL的驗(yàn)證工具verifyta.exe驗(yàn)證系統(tǒng)模型，并將輸出的驗(yàn)證結(jié)果保存在model.result中，將反例路徑保存在model.trace中。

（5）結(jié)果分析模塊：定義ResultAnalyse.py來完成，通過對(duì)model.result和model.trace文件的分析，生成分析后的結(jié)果和反例的任務(wù)調(diào)度時(shí)序圖。

另外，工具的類圖如圖6所示：

圖6 工具整體類圖

3 測(cè)試及結(jié)果分析

測(cè)試內(nèi)容設(shè)計(jì)如下：

●測(cè)試菜單欄中，各項(xiàng)（文件，幫助）功能是否正確。

●測(cè)試工具欄中，各項(xiàng)（快捷圖標(biāo)）是否正確鏈接。

●測(cè)試處理器參數(shù)設(shè)置模塊。

此后，我每周都到醫(yī)院檢查一次，到第8周的時(shí)候，醫(yī)生在我的子宮里聽到了兩個(gè)心跳的聲音，他高興地對(duì)我們說：“是雙胞胎！”我摸著自己微微隆起來的肚子，感到十分驕傲。尤其是陳清夫婦，一想到自己即將成為一對(duì)漂亮可人的雙胞胎的父母，不禁心花怒放。

●測(cè)試處理器總線參數(shù)設(shè)置模塊。

●測(cè)試實(shí)時(shí)任務(wù)描述模塊。

●測(cè)試可調(diào)度性分析模型生成模塊。

●測(cè)試可調(diào)度性分析生成的模型能否正確另存為文件。

●測(cè)試圖形化模型能否正確顯示。

●測(cè)試能否獲得正確的可調(diào)度性分析結(jié)果。

根據(jù)以上測(cè)試內(nèi)容設(shè)計(jì)了一組測(cè)試用例，結(jié)果表明設(shè)計(jì)的測(cè)試用例全部通過，一定程度上說明了工具的可用性。下面列舉兩組有代表性的測(cè)試用例，一組為輸入可調(diào)度的系統(tǒng)屬性信息，一組為輸入不可調(diào)度的系統(tǒng)屬性信息。

不可調(diào)度系統(tǒng)測(cè)試示例，如圖7，圖8，圖9所示：

圖7 不可調(diào)度系統(tǒng)屬性輸入信息圖

圖8 不可調(diào)度系統(tǒng)模型生成圖

圖9 不可調(diào)度系統(tǒng)檢測(cè)結(jié)果圖

可調(diào)度系統(tǒng)測(cè)試示例，如圖10，圖11，圖12所示：

圖10 可調(diào)度系統(tǒng)屬性輸入信息圖

圖11 可調(diào)度系統(tǒng)模型生成圖

圖12 可調(diào)度系統(tǒng)檢測(cè)結(jié)果圖

4 結(jié)語

本文針對(duì)基于概率模型檢測(cè)的多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性分析問題，開發(fā)了一個(gè)工具，實(shí)現(xiàn)可調(diào)度性分析驗(yàn)證流程的自動(dòng)化，用戶只需要輸入描述系統(tǒng)屬性的信息就可以得到可調(diào)度性分析的記錄，使得復(fù)雜的建模過程簡單化，且結(jié)果可視化。

參考文獻(xiàn)：

[1]Clarke E M,Grumberg O,Peled D.Model Checking[M].MIT Press,1999.

[2]Grolleau E.Introduction to Real-Time Scheduling[M]，2014

[3]代聲馨,洪玫,郭兵,楊秋輝,黃蔚,徐保平.多處理器實(shí)時(shí)系統(tǒng)可調(diào)度性分析的UPPAAL模型[J].軟件學(xué)報(bào),2015,02:279-296.

[4]David A,Larsen K G,Legay A,et al.Uppaal SMC Tutorial[J].International Journal on Software Tools for Technology Transfer,2015, 17(4）:397-415.

Automating Schedulability Analysis of Multiprocessor Real-Time System Based on Model Checking

DU Yi

（College of Computer Science，Sichuan University，Sichuan 610065）

Nowadays,model checking has got a rapid development,some researchers have used this technique in schedulability analysis of multiprocessor real-time system.But every different system needs different modeling,it's complex and can't be reused.For this,develops a tool to automatically analyze multiprocessor real-time system,and make the results visualized.

Model Checking;Schedulability Analysis of Multiprocessor Real-Time System;Automatically;Results Visualized

1007-1423（2017）02-0020-05

10.3969/j.issn.1007-1423.2017.02.005

杜伊（1993-），女，重慶開縣人，在讀碩士研究生，研究方向?yàn)檐浖|(zhì)量保障與測(cè)試

2016-11-22

2017-01-05