針對AADL 模型的可調度性分析方法研究

黃英蘭

(航空計算技術研究所，西安 710119)

1 引言

隨著嵌入式實時系統的廣泛應用，嵌入式系統的重要性和規模發生了重要變化。如在航空領域，嵌入式系統從聯合式發展到目前高度綜合化、模塊化的航空電子系統，傳統中的子系統被集成到多個綜合區中。為了避免整個系統綜合的不可預測性、易出錯性，避免系統前期設計的一些缺陷，近年來，美國SAE 組織為綜合化航空電子系統定義了一組滿足航空電子綜合化設計用的建模語言AADL(Architecture Analysis ＆ Design Language)。

AADL 使用軟件構件、硬件構件和系統構件描述系統的結構、使用端口、連接描述系統的連接和通信行為，使用各種屬性來描述系統的功能和非功能屬性。使用AADL 建立嵌入式實時系統模型后，可以對模型的各種非功能屬性進行分析、仿真系統的行為、生成指定目標語言的源代碼。使得過去只能夠在系統實現后，才能驗證的非功能性屬性驗證提前到系統設計階段，提高了系統設計的正確性和可靠性。通過自動代碼生成避免了手工編碼的費時、費工和易出錯性，最終得到滿足功能和性能要求的系統。

近年來很多國內外研究機構積極投身于對AADL 語言的研究，并開發了多種支持AADL 建模、模型轉換、性能分析、模型仿真和自動代碼生成的工具。卡內基.梅隆大學下屬的軟件工程學會開發的一套支持使用AADL 進行綜合建模、分析的開源工具集OSATE(Open Source AADL Tool Environment)就是其中最具代表性的工具集。

本文重點關注使用AADL 語言建立的嵌入式實時系統模型的可調度性。首先對AADL 語言進行概述，重點對可調度性分析工具可能使用到的屬性進行簡要介紹。然后針對幾種使用AADL 模型進行可調度性分析的工具進行介紹，分析它們的優缺點，為使用者選擇合適的分析工具提供依據。最后對可調度性分析工具的發展提出自己的看法。

2 AADL 語言概述

SAE的AADL是用于設計和分析性能關鍵實時系統的軟、硬件結構的一個文本和圖形語言［1］。這些系統的運行依賴于滿足像可靠性、可用性、時序、響應率、吞吐率、安全性這些非功能的系統需求。

AADL 語言使用構件來表示要建模系統中的軟、硬件實體。它定義了下面一些構件:數據、子程序、線程、線程組、進程、處理器、存儲器、總線、設備和系統。其中軟件構件有:數據、子程序、線程、線程組和進程構件;硬件構件，即執行平臺構件有:處理器、存儲器、總線和設備構件。AADL 語言使用端口、連接來描述構件間的功能接口。端口有數據端口、事件端口、事件數據端口。使用綁定來描述軟件構件到硬件構件的映射。使用模式和模式轉換來描述運行系統的動態行為。AADL 語言還支持使用附件庫和附件子句對核心語言進行擴展。例如，通過添加錯誤模型附件來支持對模型進行可靠性分析，通過使用屬性來描述構件的性能指標。

對AADL 模型進行可調度性分析可能使用到的屬性有:

·Activate_Deadline:指定允許的執行線程活動的最大時間;

·Activate_Execution_Time:指定了在沒有運行錯誤出現的情況下，線程執行它的活動序列所需的最小和最大執行時間;

·Actual_Processor_Binding:指定了線程所綁定的處理器;

·Allowed_Period:指定了允許綁定到某個處理器上周期任務的周期集合;

·Allowed_Processor_Binding:指定了線程允許綁定的處理器;

·Clock_Period:指定了處理器或系統的兩個時鐘中斷之間的時間值;

·Clock_Period_Range:指定了Clock_Period 最大和最小值;

·Compute_Deadline:指定了執行一個線程計算序列的最大時間;

·Compute_Execution_Time:指定了在一個線程派發后和在下一次派發前一個線程執行的時間范圍;

·Deadline:指定了一個線程派發的時間和線程開始等待另一次派發的時間之間的最大時間;

·Dispatch_Protocol:指定了一個線程的派發行為;

·Period:當線程的調度協議為周期或零散的協議時，指定了兩次派發之間的時間間隔;

·Scheduling_Protocol:指定了處理器的線程調度器使用的調度協議。

對AADL 模型進行可調度性分析將可能使用到上述的屬性。在使用時，可以參考文獻［1］來詳細了解屬性的含義、適用的構件類型。本文所分析的可調度性分析工具有Scheduling、VERSA、aadl2sync、Cheddar 工具。

3 Scheduling

Scheduling是集成到 OSATE (Open Source AADL Tool Environment)工具集中的可調度性分析工具。OSATE是由軟件工程學會為AADL 開發的基于Eclipse的集成開發環境［2］。集成在該環境下的可調度性分析插件以AADL 描述的一個系統實例為輸入進行可調度性分析，只支持最早截止期優先(EDF)、速率單調算法(RMS)的分析，目前它還只是一個示例性的插件，功能還較為簡單。

用戶可以通過點擊Analyses－ ＞Scheduling－ ＞Bind and schedule threads 菜單來啟動綁定和調度線程插件，此插件嘗試在系統實例中綁定線程實例到處理器實例，以線程的Period、Deadline、Clock_Period、Scheduling_Protocol 和allowed_processor_binding屬性為輸入。如果線程可以在該處理器中調度，此插件報告線程和處理器的綁定，并返回處理器的利用率。由于需要使用獨立于處理器的計算執行時間，因此該插件將線程的執行時間轉換為時鐘周期個數。該插件實現了EDF 和RMS 調度協議。如果沒有指定協議，則默認是EDF。例如，針對兩個線程綁定到一個處理器上的例子，該例子的AADL 文本表示如下，分析結果如圖1 所示。

圖1 OSATE 中集成的可調度性分析工具分析結果圖

目前該插件也只是一個示例性的插件，軟件工程學會計劃下一步擴充該插件的功能，使得該插件支持更多的調度算法，支持對模型的不同模式進行可調度性分析。并且該插件可以與已有的調度性分析工具連接，將AADL 模型生成已有模型識別的模型表示，例如，可以生成一個針對TimeWiz的時序模型(TimeWiz是一個商用調度性分析執行跟蹤分析工具)，調用該工具，分析結果顯示在該工具中，但將結果狀態映射回AADL 環境中。

4 VERSA

VERSA(Verification Execution and Rewrite System for ACSR)是賓夕法尼亞大學開發的使用ACSR(Algebra of Communicating Shared Resources)來進行資源有限的實時系統的自動分析工具［3］。ACSR 能夠對敏感資源進行描述，還能夠對系統的時序限制進行描述。ACSR 還包括資源、時序和優先級的精確概念。

VERSA 使用ACSR 來構造和分析系統，它具有下列特征:

·支持ACSR的完全語法和語義;

·支持過程表示的語法和語義檢查;

·支持對過程的等值檢測;

·支持與ACSR 過程對應的系統交互執行。

VERSA 對ACSR時序屬性的分析包括對任意任務模型的可調度性分析，如多處理器和資源、任務依賴。VERSA 實現了:①ACSR的語義;②狀態空間的探測，死鎖的檢測;③診斷結果是失敗場景。對時序和資源分析包括將資源沖突視為死鎖，允許編輯任務模型、調度策略、內部任務的依賴。

目前賓夕法尼亞大學研究利用VERSA的功能來分析AADL 模型的可調度性，并開發了VERSA 插件集成到OSATE 平臺中。該插件的示意圖如圖2 所示。該插件首先將AADL 模型轉換為ACSR 模型，然后利用VERSA 已有的功能進行AADL 線程的可調度性分析，并將分析結果返回到OSATE 平臺中。在AADL 模型轉換到ACSR 模型時，將基于線程的語義自動機線程建模為ACSR 進程;處理器和訪問鏈接建模為資源;事件和數據連接建模為通信通道。

圖2 OSATE 中集成的VERSA 插件示意圖

此插件實現了將AADL 模型轉換、可調度性分析、結果顯示的功能，使得用戶可以不用切換工具環境即可進行從建模到分析的工作。但是沒有證明兩種模型的等價性。

5 aadl2sync

aadl2sync 工具集支持對AADL 模型進行仿真和形式化驗證［4］，它能夠仿真模型的調度方法，目前的版本支持仿真速率單調調度方法。給定AADL模型和構件實現，aadl2sync 支持執行自動仿真和形式化驗證。這是通過轉換AADL 模型為Lustre 編程語言來實現的，利用仿真和形式化驗證工具鏈，來執行仿真驗證。此工具鏈允許設計者在機器代碼生成和開發階段的早期就關注于功能屬性。該轉換的主要困難是建模不確定和將異步AADL 描述為一個同步語言。為了達到此目的，aadl2sync 使用基于零散活動條件、輸入條件和類同步時鐘的技術。

在轉換時，AADL 模型與Lustre 節點的對應關系如下:

·AADL 系統構件:轉換為Lustre的一個高級節點，系統的每個輸入端口映射為Lustre 節點的一個輸入。系統實現中的每個子構件映射為一個Lustre節點;

·硬件構件:設備構件用于AADL 模型與外部環境進行連接，因此設備的輸入作為系統輸出，設備的輸出作為系統輸入。處理器是用于執行和調度進程的硬件和軟件的一個抽象。Clock_period 屬性聲明處理器內部的時鐘頻率，在轉換時用于建模處理器時鐘之間的關系。在系統包含幾個處理器時，使用Clock_period 來生成類同步時鐘;

·內存構件:轉換時用于指定其他構件可以使用的內存類別和大小;

·總線構件:轉換時將它視為通常的連接來看;

·進程構件:轉換時作為調度和執行線程的一個抽象軟件;

·線程構件:轉換時作為調度和執行線程的一個抽象軟件;

·數據構件:轉換時作為Lustre 類型，而不是Lustre 節點。

目前aadl2sync 對有些AADL 模型概念還不支持，例如包含輸入和輸出的端口組、作為系統子構件的系統、線程組、模式、零散、非周期和后臺線程、執行故障處理的線程等概念。aadl2sync 對AADL 支持的詳細介紹可以參考文獻［4］。

aadl2sysnc是獨立可執行的工具。Aadl2sync 并不以aadl 文件作為輸入，而是以aadl 文件對應的aaxl 文件作為輸入。此aaxl 文件可以通過使用OSATE 工具集中的插件來獲得。啟動aadl2sysc 工具來處理某個aaxl 模型文件，將編譯生成6個文件:

文件名.lus:包含高層次的Lustre 節點文件，可分別用于仿真和形式化驗證;

文件名_nodes.lus:包含模型中所有AADL 構件的Lustre 表示;

文件名_scheduler.lus:包含在翻譯時引入的驅動所有計算的調度器;

fillme_文件名_nodes.lus:包含與aadl 模型葉節點對應的節點接口。需要提供這些節點的實體;

fillme_文件名_const.lus:包含各種需要定義的常量，例如構件初始值;

fillme_文件名_types.lus:包含數據類型構件的Lustre 類型定義。

該轉換目前還沒有做到自動化。后面的3個以前綴fillme 開頭的文件需要填充，填充完成后要將前綴刪除進行重命名。作為任何一個xml 文檔，aaxl文件應該在文件頭定義URI 用來查找它們滿足的xml schema，但是由OSATE 生成的aaxl 文件定義了一個錯誤的URI(http://AADL/)。為了逆轉這個問題，aadl2sync 拷貝了那些schema 文件到/tmp/aadl－schema/路徑。因此，只需要修改aaxl 文件使得它指向該路徑即可。

aadl2sync 工具集只能夠以后綴為aaxl的AADL模型文件為輸入進行仿真，它不具有建模功能，也不具有證明兩種模型等價性的功能，而且目前還有一些AADL 模型概念不支持。

6 Cheddar

Cheddar 由布雷斯特大學開發，是一個免費的實時調度框架［5］。它是由Ada 語言實現的框架，能夠檢查一個實時應用是否滿足它的時間限制。在Cheddar 中，一個應用由處理器、任務、緩存、共享資源和消息的集合組成［6］。Cheddar為單處理器、多處理器和分布式系統提供了方便的時間可行性分析。它也提供了一個方便的仿真機制，允許設計者描述和運行特定系統的仿真。該框架是開放的，并且便于與CASE(計算機輔助軟件工程)工具，例如編輯器、設計工具、仿真器等工具連接。

開發Cheddar 主要為了三個目的:

(1)提供一個實現大多數傳統實時調度原理方法的工具。可行性測試可應用于單處理器和分布式系統的常用調度方法，如最早截止期優先、截止期單調、最早松弛度優先和POSIX 調度器的SCHED_FIFO、SCHED_RR、SCHED_OTHERS 隊列策略。可行性測試也關注于任務間共享緩存或任務搶占系統。人們可以通過Cheddar 來研究實時調度原理的基礎;

(2)提供一個開放的、輕便的和易使用的工具。對于那些對實時調度原理沒有概念的人該工具也很方便使用。因為開放性，該工具容易與其它工具，如仿真器、CASE 工具、監控服務器等連接。該工具的輸入和所有輸出都是XML 格式的。為了輕便性和可維護性，使用Ada 語言來實現該框架;

(3)提供一個靈活的擴展。可行性測試僅僅支持幾個已知的調度方法，而Cheddar 仿真器可以靈活的仿真具有特定時序行為的系統。用戶可以使用類Ada的仿真語言來擴展該工具，使用該語言描述的用戶擴展并不被編譯，而是在仿真時由工具進行解釋。這使得設計者在不是很深入了解工具設計和Ada 語言的基礎上也可以快速的編寫和測試新的調度特征。

Cheddar 提供了工具來檢查AADL 線程是否在執行時滿足它們的截止期［7］。它可以將AADL 描述轉換為Ada 描述來執行可調度性分析。大部分Cheddar的可調度分析服務可以直接應用于AADL描述。然而，為了支持其它一些實時調度分析算法，需要添加一些額外的AADL 屬性。

在Cheddar 中，一個應用由處理器、緩存、共享資源、消息和任務的集合組成。對這些任務集合，在Cheddar 中可以執行可調度性仿真和可行性分析。調度仿真結果由任務分配的處理器的時間單位組成，如果任務滿足它們的截止期，Cheddar 繼續執行計算。圖3 給出了一個使用Cheddar 進行可調度性仿真分析的例子，在該例子中有3個周期任務(T1、T2 和T3)，周期分別為10、20、35，執行時間分別為3、8、7，截止期為10、20、35，這三個周期任務運行在同一處理器上，使用速率單調調度(RATE_MONOTONIC_PROTOCOL)方法。在窗口的上部，顯示了調度仿真結果。這些任務以可搶占的單調速率方法可調度。

圖3 Cheddar 調度仿真結果示例

在可調度性分析后，可以抽取出最好、最壞、平均情況下的響應時間，阻塞時間、搶占次數、上下文轉換次數、端對端消息通信延遲等。給定一個任務集合，如果難以執行調度仿真，Cheddar 將使用可行性測試代替仿真給出可行性測試結果。目前cheddar 提供3種可行性測試:基于處理器利用率的測試、任務響應時間滿足任務截止期測試、緩存利用率測試。詳細的使用方法可參考文獻［6］。

Cheddar 支持以AADL 模型為輸入，進行可調度性分析和仿真，并且支持定制特定調度方法的分析和仿真，界面簡單、易學易用，但是不支持建模，也不能夠直接與建模工具集成。

7 結束語

從對上述工具的研究來看，目前針對AADL 模型進行可調度性分析主要有兩種方式。第一種方式是直接設計實現針對AADL 模型的可調度性分析工具，如OSATE 工具集中的Scheduling;第二種方式是將AADL 模型轉換為其它模型，利用針對其它模型的可調度性工具進行可調度性分析，這種方式要考慮兩種建模語言的差異，轉換后模型的一致性問題，如VERSA、aadl2sync、Cheddar。對AADL 模型進行可調度性分析使用的方法有兩種:第一種是根據模型所采用的調度方法進行靜態分析，給出是否可調度的結論，如OSATE 中的Scheduling、VERSA;第二種是采用仿真的方法給出是否可調度結論，如aadl2sync。而Chedda 既可以采用分析，也可以采用仿真方法對模型的時序進行分析，并且Chedda 提供了方便、靈活的機制，允許使用者根據需要來對一種新的調度方法進行可調度性分析和仿真。

雖然目前針對AADL 模型的可調度性分析工具多種多樣，但是集AADL 建模與分析為一體的建模工具卻不是很多，目前只有OSATE、STOOD 具有此功能。其它分析工具都不具有AADL 建模功能，只能以AADL 模型為輸入，進行分析。而且大多數分析工具也只是針對一些常用的調度方法進行分析。

為了方便使用，后續需要繼續研究各種工具的集成問題，以及針對近年來關注較多的調度方法，如層次調度方法的研究。

［1］Peter Feiler.Architecture Analysis ＆ Design Language(AADL)［S］.Carnegie Mellon University:SAE Aerospace，2004.

［2］Software Engineering Institute ，Open Source AADL Tool Environment (OSATE)Online Help［R］.Carnegie Mellon University :Software Engineering Institute，2006.

［3］Duncan Clarke，VERSA:Verification，Execution and Rewrite System for ACSR［R］.Technical Report of University of Pennsylvania，1995.

［4］Erwan Jahier，Louis Mandel，Nicolas Halbwachs，and Pascal Raymond.The AADL2sync User Guide［R］.Unite Mixte de Recherche CNRS，2008，http://www－ verimag.imag.fr/DIST－TOOLS/SYNCHRONE/aadl2sync/aadl2sync－man.pdf.

［5］Frank Singhoff，Jér?me Legrand，Laurent Nana，Lionel Marcé，Cheddar 1.3 user＇s guide［R］.EA 2215 Team，2006，http://beru.univ－ brest.fr/～singhoff/cheddar/ug/cheddar－r1.pdf.

［6］F Singhoff，J Legrand，L Nana，L Marc＇e.Cheddar:a Flexible Real Time Scheduling Framework［C］.Proceedings of the ACM SIGADA International conference Proceedings，Atlanta，Georgia，USA，2004.

［7］F Singhoff，J Legrand，L Nana，L Marc'e.Scheduling and Memory requirements analysis with AADL［C］.Proceedings of the ACM SIGADA International conference Proceedings，Atlanta，Georgia，USA，2005.