基于模型檢測的多處理器實時系統可調度性自動化分析

杜伊

（四川大學計算機學院，成都 610065)

基于模型檢測的多處理器實時系統可調度性自動化分析

杜伊

（四川大學計算機學院，成都 610065)

近年來，模型檢測技術獲得快速的發展，已有學者將模型檢測技術用于多處理器實時系統可調度性分析。但如果對每個實際系統都手工建立模型進行可調度性驗證，過程繁瑣且模型不可重復利用。針對此，開發一個工具用于自動完成可調度性檢測，并可視化顯示結果。

模型檢測技術；多處理器實時系統可調度性；自動化；可視化

0 引言

模型檢測[1]是一種形式化驗證方法，通過自動地窮盡搜索待驗證系統的狀態空間，驗證系統是否滿足給定的性質，并在系統不滿足性質時給出違背性質的反例。

如果一個實時任務的響應時間小于或等于它的截止時間，我們稱這個任務是可調度的?？烧{度性分析[2]就是驗證給定的系統環境中所有的任務是否都可調度的一種重要方法。

已有學者[3]將概率模型檢測用于多處理器實時系統可調度性分析，但這一過程需要手動建立模型，且模型不可重復利用，對不同的多處理器實時系統需要手動改變模型以達到驗證的目的。同時，現有的模型檢測工具和技術都要求使用者了解形式化的語言，才能對驗證系統進行描述，建模困難問題給模型檢測的廣泛應用帶來一定阻礙。

基于此，本文開發了一個工具，實現可調度性分析驗證流程的自動化，提供配置系統和任務的接口，將描述的系統設計建立成模型檢測工具UPPAAL[4]的驗證模型，并自動執行檢測過程，獲得驗證結果后進行進一步分析，若生成反例則將反例有效信息提取出來形成任務調度的時序圖，通過提供的輸出接口向用戶展示分析后的可視化結果。

1 系統問題-模型對應關系

多處理器實時系統由實時任務、運行平臺以及任務調度模塊組成，其中，實時任務包含一組周期性任務以及任務之間的依賴關系，系統運行平臺包括多個處理器和連接處理器的總線，任務調度管理模塊即系統維護的調度策略和調度序列等。對于實時任務調度問題中的每個部分，使用UPPAAL模型中的模型或數據結構來建模表示，問題與模型的對應關系如圖1所示。

圖1 問題-模型對應關系圖

任務模板為Task，根據系統實際情況可以使用具體的參數(任務屬性)實例化多個任務；依賴管理器為DenpendencyManager，處理任務間的依賴關系，總線模板為Bus，處理器被抽象為一個數組，并作為調度器的參數可以根據實際系統進行配置具體的值；調度管理模塊抽像為調度器模板Scheduler和策略模板Policy，支持多種策略模板，通過Scheduler實現處理器和調度策略的關聯，將處理器和調度策略分開建模的好處是可以更方便地擴展調度策略。

2 自動化工具設計

2.1 需求分析

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

圖2 工具的用例圖

系統可調度性自動化分析工具活動圖如下：

圖3 工具的活動圖

用戶輸入描述系統信息界面：輸入是詳細的系統描述信息，包括任務屬性、任務依賴關系、處理器屬性、總線屬性等信息，可以是用戶手動輸入的內容，也可以是直接打開的可擴展名為.data的文件，若該系統可調度，那么輸出只有一項，即結果文件Model.result，并告知用戶系統是可調度的；若該系統不可調度，則輸出有兩項：結果文件Model.result和反例路徑Model.trace，并可視化的顯示任務調度時序圖。

2.2 詳細設計

開發環境：

●CPU：AMD AthlonII X4 640 3.0GHz

●RAM：3.0G

●操作系統：Microsoft Windows 8

●模型檢測工具：UPPAAL 4.1.18

●開發工具：Python-2.7，Pyqt4

嵌入式系統實時任務可調度性分析子系統設計結構如圖4所示，組件設計如圖5所示：

圖4 工具整體設計結構圖

圖5 工具組件設計圖

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

（1）圖形用戶界面：接收用戶輸入，反饋驗證結果主要包含以下三個文件：

●ScheduleWindow.py主要負責用戶輸入系統信息界面的顯示；

●ScheduleModelResultWindow.py主要負責建立好的模型文件的顯示；

●ScheduleAnalysisResultWindow.py主要負責可調度性驗證結果的顯示。

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

（4）模型驗證模塊：定義一個Controller.py文件來完成，功能是調用UPPAAL的驗證工具verifyta.exe驗證系統模型，并將輸出的驗證結果保存在model.result中，將反例路徑保存在model.trace中。

（5）結果分析模塊：定義ResultAnalyse.py來完成，通過對model.result和model.trace文件的分析，生成分析后的結果和反例的任務調度時序圖。

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

圖6 工具整體類圖

3 測試及結果分析

測試內容設計如下：

●測試菜單欄中，各項（文件，幫助）功能是否正確。

●測試工具欄中，各項（快捷圖標）是否正確鏈接。

●測試處理器參數設置模塊。

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

●測試處理器總線參數設置模塊。

●測試實時任務描述模塊。

●測試可調度性分析模型生成模塊。

●測試可調度性分析生成的模型能否正確另存為文件。

●測試圖形化模型能否正確顯示。

●測試能否獲得正確的可調度性分析結果。

根據以上測試內容設計了一組測試用例，結果表明設計的測試用例全部通過，一定程度上說明了工具的可用性。下面列舉兩組有代表性的測試用例，一組為輸入可調度的系統屬性信息，一組為輸入不可調度的系統屬性信息。

不可調度系統測試示例，如圖7，圖8，圖9所示：

圖7 不可調度系統屬性輸入信息圖

圖8 不可調度系統模型生成圖

圖9 不可調度系統檢測結果圖

可調度系統測試示例，如圖10，圖11，圖12所示：

圖10 可調度系統屬性輸入信息圖

圖11 可調度系統模型生成圖

圖12 可調度系統檢測結果圖

4 結語

本文針對基于概率模型檢測的多處理器實時系統可調度性分析問題，開發了一個工具，實現可調度性分析驗證流程的自動化，用戶只需要輸入描述系統屬性的信息就可以得到可調度性分析的記錄，使得復雜的建模過程簡單化，且結果可視化。

參考文獻：

[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]代聲馨,洪玫,郭兵,楊秋輝,黃蔚,徐保平.多處理器實時系統可調度性分析的UPPAAL模型[J].軟件學報,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-），女，重慶開縣人，在讀碩士研究生，研究方向為軟件質量保障與測試

2016-11-22

2017-01-05