基于體系結構模型的綜合化航電分區可調度性驗證

劉哲旭 樊智勇 趙 珍

1(中國民航大學電子信息與自動化學院 天津 300300)2(中國民航大學工程技術訓練中心 天津 300300)

0 引 言

現代新型飛機電子設備已快速進入綜合模塊化航空電子系統(Integrated Modular Avionics，IMA)的嶄新時代[1]。在民用航空領域，歐洲Airbus和美國Boeing均率先將先進的IMA航電架構應用于新一代民用客機(A380和B787)，而我國的國產大型客機C919也將航電系統的綜合模塊化技術作為飛機研制的關鍵。

IMA作為安全關鍵的復雜嵌入式系統，其軟件系統的可靠性和安全性是保證飛行安全的必要條件[2-5]。為此，IMA軟件接口開發規范ARINC653將“分區”作為系統軟件開發的核心理念。這種方式可以隔離資源分配和應用，避免了應用間錯誤的相互影響，從而提高了系統的容錯性。然而，由于IMA采用了分區層調度和任務層調度的雙層調度機制，這使得系統中任務的調度和執行更加復雜，傳統的可調度分析方法已不再適用[6-7]。

近年來，模型驅動的開發方法(Model driven development，MDD)在IMA等復雜嵌入式系統的設計和驗證領域得到了廣泛應用。由于其能夠在開發階段對系統進行分析與驗證，有助于保證系統的質量屬性，并可以有效地控制開發時間與成本。目前，針對IMA系統的分區調度問題，基于MDD的方法已取得了一些研究成果。文獻[8]采用統一建模語言(Unified Modeling Language，UML)建立了IMA軟件系統的分區調度過程模型，提出了分區配置和啟動機制的設計策略。文獻[9-10]采用實時嵌入式系統建模與分析語言(modeling and analysis of real time and embedded systems，MARTE)對IMA的分區調度問題進行研究，通過建立系統的MARTE模型對IMA分區的時間資源配置進行了驗證。但是，由于上述方法在本質上都是多模型多分析的方法，其在分析系統不同屬性時所建立的模型存在不一致性，這不利于復雜嵌入式系統的整體驗證[11]。

體系結構分析與設計語言(Architecture Analysis & Design Language，AADL)是由美國汽車工程師協會于2004年提出的一種用于嵌入式實時系統設計和開發的MDD工具。與上述方法相比，AADL只需通過建立單一模型即可支持系統多種關鍵屬性的分析，可以將系統的分析和驗證融合于統一框架之下，因此，已逐漸成為IMA等復雜嵌入式系統關鍵屬性驗證的標準建模語言[12-15]。目前，針對復雜嵌入式系統AADL模型的可調度性驗證方法均采用了模型轉換的方式。文獻[16-17]在建立系統AADL模型的基礎上，討論了AADL模型到時間自動機的轉換，并使用UPPAAL工具實現了可調度驗證。文獻[18]將IMA分區資源配置的AADL模型轉換為著色Petri網模型，通過著色Petri網描述了AADL模型中的時間資源和物理資源，并可在此基礎上進行分區可調度性驗證。然而，上述方法中的AADL模型均不能描述系統中任務調度的動態行為，因此不能直接用于系統的可調度性驗證。驗證時，還需要對AADL模型進行轉換或二次建模，這一過程是比較繁瑣的。

為解決上述問題，本文提出了基于AADL的IMA分區可調度性驗證模型的建模方法，并在此基礎上對其可調度性驗證方法進行研究，避免了現有方法中繁瑣的二次建模過程。

1 IMA分區調度原理

1.1 IMA分區架構

ARINC653標準中定義的IMA架構如圖1所示，與一般嵌入式系統類似，由硬件和軟件兩部分組成。圖1中，IMA模塊的軟件部分可以進一步劃分為分區應用軟件與核心軟件(ARINC653操作系統)。其中，分區應用軟件用于實現航空電子設備的各種特定功能，如飛行管理、飛行控制、通信導航等。核心軟件將分區應用軟件與硬件環境隔離開，同時也為應用軟件的運行提供通信、調度等各種底層服務。一般來說，為了滿足各種功能需求，IMA系統中的分區應用軟件數量很多，而作為核心軟件的操作系統往往只有一個，分區應用軟件與核心軟件間的信息傳遞是通過應用可執行接口(APplication/EXecutive，APEX)來實現的。

圖1 ARINC653標準定義的IMA架構

ARINC653標準定義的IMA軟件系統將分區作為其核心理念。模塊被劃分為若干個分區，并給每個分區分配了指定的內存空間和處理器時間片等資源。在此基礎上，分區應用軟件的各種功能可以通過調度部署在不同分區內的任務進程來實現。本文研究的IMA分區可調度性即為其中分區應用軟件的關鍵特性。

1.2 分區調度機制

根據ARINC653標準，IMA系統中對于分區應用軟件采用了雙層調度機制，如圖2所示。操作系統層進行分區層調度，分區調度器對處理器時間進行分派，以時間片輪轉的方式來激活各分區。在此基礎上，應用軟件層進行任務層調度，各分區被激活后，其中的任務調度器按照配置好的策略來調度相應的任務集，從而完成各應用軟件的功能。

圖2 IMA分區應用軟件的雙層調度機制

(1) 分區層調度。分區層調度為上層調度機制，是指操作系統對各分區的調度。分區層調度機制如圖3所示。

圖3 IMA分區層調度

分區層調度采用了循環調度算法(Round-Robin，RR)，這是由系統配置文件所決定的，是固定不變的。如圖3所示，分區之間沒有優先級之分，在一個主時間框架內，所有分區都會至少分配到一個系統時間片，且每個分區獲取系統時間片的周期和長度均為定值。

(2) 任務層調度。任務層調度為下層調度機制，是指在分區分派的時間片內對其內部的任務進程進行調度。

與分區層調度不同，任務層調度采用基于優先級的可搶占式調度策略，例如最早截止期優先算法(Earliest Deadline First，EDF)、時限單調調度算法(Deadline-Monotonic Scheduling，DMS)和速率單調調度算法(Rate-Monotonic Scheduling，RMS)等。在任務層調度中，每個任務都被賦予一個優先級，任務調度器始終將時間片分配給當前優先級最高的任務。如在任務執行期間，某一更高優先級任務被調度，則立即停止當前任務，執行高優先級任務，并在高優先級任務結束后再恢復執行當前任務。

綜上所述，IMA系統的分區調度機制可概括為：操作系統將處理器時間片按照固定的周期和順序分派給各分區；各分區下的任務進程則按照其自身優先級搶占分區時間片。需要注意的是，當某分區獲得的處理器時間片截止時，其中的任務進程也會立即失去調度并暫停執行，直到該分區再次獲取系統時間片后再恢復執行。

為了保證IMA系統的安全運行，各分區中任務的執行均應在其截至期限前完成，即需要具備充分的可調度性。然而，由于任務層調度中采用了優先級搶占式調度策略，各任務獲取時間片的周期和長度是由其自身的約束條件(執行時間、截止時間、優先級)決定的，這極大提高了調度過程的復雜程度，系統的可調度性難以直接判定。本文即針對IMA系統的分區可調度性驗證方法進行研究。

2 分區調度與AADL元素映射規則

本文提出的IMA分區可調度性驗證方法是基于AADL建模語言所構建的體系結構模型實現的。因此，需首先建立IMA分區調度的主要概念與AADL中的各類組件、屬性等建模元素之間的有效的語義映射。

AADL定義了3類組件：軟件組件，包括數據(data)、線程(thread)、進程(process)和子程序(subprogram)；執行平臺組件，包括處理器(processor)、虛處理器(virtual processor)、存儲器(memory)、總線(bus)、虛總線(virtual bus)和外設(device)；系統組件可將所有的組件整合，層次化地建立系統的體系結構。為滿足不同的應用需求，AADL還引入了附件的概念，如用于故障事件及屬性建模的錯誤附件(Error model Annex)和用于實際功能行為建模的行為附件(Behavior Annex)。

結合IMA分區調度原理，本文建立的模型語義映射規則如表1所示。

表1 AADL與IMA分區調度的模型語義映射規則

AADL處理器組件可以描述分區和任務的執行環境，其與IMA分區調度中的操作系統概念相同。其中，考慮到各分區均需要獨立的執行環境，因此通過虛處理器子組件將處理器組件分成相互獨立的邏輯資源。

分區映射為AADL進程組件，且需將不同分區綁定相應的虛處理器子組件和內存組件。其中，內存組件用于描述執行分區的內存要求，并通過虛處理器子組件的屬性來描述分區層調度策略。

AADL進程組件中往往包含一個或多個作為基本執行單元的線程組件，可以用來表示任務的執行，因此將任務映射為線程組件。

行為附件是AADL的延伸，其可以通過代碼描述系統對分區中各任務的調度操作，因此將任務層調度策略映射為行為附件模型。

3 IMA分區可調度性驗證模型

根據上述映射規則，本文建立了IMA系統分區的可調度性驗證模型。在靜態體系結構模型的基礎上，通過建模其動態行為來描述任務調度過程，分別為分區架構模型和分區調度策略模型。

3.1 分區架構建模

為方便討論，以用于實現大氣數據溫度傳輸的某應用軟件的分區調度為例，闡述本文所提出的建模與驗證方法，相關參數如表2所示。

表2 IMA系統分區參數

表2中給出了該系統在主時間框架為30 ms下的分區和分區內任務的調度情況。該系統含有P1和P2兩個分區，其中所采用的任務層調度策略分別為DMS和RMS。P1和P2分配的時間片長度分別為20 ms和10 ms。兩個分區中各包含2個任務，并規定了相應的周期、執行時間和截止時間。

根據第2節中提出的模型映射規則，構建該系統分區架構的AADL模型，如圖4所示。

圖4 分區架構AADL模型

圖4中，IMA的操作系統由AADL處理器組件“CPU”描述，其中包含兩個虛處理器子組件“Virtual_processor_P1”和“Virtual_processor_P2”。系統的兩個分區分別用AADL進程組件“Partition1”和“Partition2”進行建模，并綁定到相應的虛處理器和內存，綁定關系由帶箭頭的虛線表示。分區中的各任務則分別映射為AADL線程組件“Order”、“Temperature_capture”、“Printer”、“Receiver”。此外，本文研究對象為IMA系統的分區和任務的調度，因此忽略任務間的數據傳輸，將其簡化為事件觸發<>，在圖4中用實線表示。

3.2 分區調度策略建模

針對IMA系統的兩層調度機制建立其分區調度策略的AADL模型。

(1) 分區層調度建模。由1.2節可知，IMA系統的分區層調度采用了RR調度算法，各分區按照固定周期輪流獲取處理器時間片。根據表2中給出的主時鐘框架周期和分區時間片，構建其分區層調度策略模型，如圖5所示。

(a) 分區層調度策略 (b) 分區層調度策略模型圖5 分區層調度策略建模

建模時通過AADL虛處理器子組件的3個屬性來描述分區層調度策略。以分區1為例，在圖5(b)中，“Dispatch_Protocol=>Periodic”表示采用周期固定的循環調度算法，“Period=>30 ms”定義分區調度周期即主時鐘框架為30 ms，“Execution_Time=>20 ms”定義分區1所獲取的處理器時間片為20 ms。

(2) 任務層調度建模。為解決現有方法不能有效描述IMA分區兩層調度機制的問題，本文基于AADL的行為附件構建了任務層調度策略模型，并通過行為附件描述了分區內任務復雜的調度操作。

針對IMA系統任務層所采用的基于優先級的搶占式調度策略，并結合AADL行為附件的建模特性，設計相應的任務調度模型的執行流程如圖6所示。

圖6 任務調度模型的執行流程

由圖6可知，當判定任務被調度后，系統將其置入任務隊列，并在隊列中按優先級對所有任務進行排序。在隊列中處于首位的任務優先級最高，其將立即執行。任務執行完成后，系統會將其移出任務隊列，等待下一次調度。另外，如果某任務運行時，系統調度了另一優先級更高的任務，則當前任務將暫停執行并掛起，直到其再次成為隊列中優先級最高的任務時才能恢復執行。其中，判定當前任務執行過程中是否有更高優先級任務被調度的時間間隔設定為1 ms，其取自表2給出的各任務的調度周期和執行時間的最大公約數。針對不同分區參數，該值可根據情況做相應改變。

根據圖6，基于AADL行為附件對分區中的全部任務分別建模，構建IMA系統任務層調度策略模型。以任務“Temperature_capture”為例，其偽代碼如圖7所示。

圖7 基于AADL行為附件的任務層調度策略模型

圖7中，在AADL線程組件“Temperature_capture”的屬性中定義了該任務的調度周期和截止時間，其調度行為則通過AADL行為附件中定義的狀態轉換過程來進行描述。

其中，行為附件模型代碼中的“states”部分定義了5個狀態：“Initial”為起始待命狀態，“WaitRun”表示任務被調度后的等待運行狀態，“Running”為任務執行狀態，“HangUp”表示任務被搶占后的掛起狀態，“Complete”為任務執行完成狀態。

“transitions”部分通過上述狀態的轉換來描述任務調度過程。其中為實現相應功能定義了3個子程序：“enqueue()”用于將任務置入隊列并進行優先級排序，“priority_test()”用于判定該任務是否為當前最高優先級,“dequeue()”用于在任務執行結束后將其移出隊列。

4 IMA分區可調度性驗證

本文采用AADL Inspector工具，基于模型分析的方法對IMA分區的可調度性進行評估。AADL Inspector提供了一套模型分析平臺，不僅可以驗證AADL模型的靜態結構，也可以基于處理器利用率對其動態行為進行分析。由于本文所建立的IMA分區可調度性驗證模型中已經對其調度行為進行了描述，因此，與傳統方法相比，在進行可調度性驗證時就不需要再對模型進行二次轉換。

4.1 架構正確性驗證

對于模型架構正確性的驗證主要考察其是否正確描述了IMA系統的航電分區架構以及是否符合AADL建模規則。本文通過AADL Inspector的靜態分析工具對所建模型進行驗證，將上述模型作為AADL Inspector的輸入，分析結果如下所示。

圖8為所建模型的統計聲明，其中給出了系統模型的組件數量以及組件屬性的統計。由圖8中給出的結果可知，模型中的處理器組件、進程組件和線程組件的數量均與表2中規定的分區參數一致。

圖8 模型統計聲明

圖9為調用邏輯模型處理算法(Logic Model Processing，LMP)對模型中建模規則一致性的驗證結果。該結果表明模型無建模規則錯誤。

圖9 規則一致性驗證

圖10為調用LMP算法對模型中的語法限制進行驗證。該結果表明模型符合AADL語法規則，無語法錯誤。

圖10 語法合法性驗證

圖11為對模型中組件元素的命名規則和名稱引用是否正確進行驗證。該結果表明模型無命名規則錯誤。

圖11 命名正確性驗證

圖12為對模型是否符合ARINC653標準中規定的軟件架構規則進行驗證。該結果表明模型無ARINC653規則錯誤。

圖12 ARINC653一致性驗證

通過上述靜態驗證結果可知，本文方法構建的分區可調度性驗證模型能夠正確描述系統體系結構且符合相應建模規則。

4.2 可調度性驗證

分區可調度性驗證是本文關注的重點問題，主要考察IMA系統分區和任務是否滿足可調度性。判定條件為：如果某任務在每一次被調度后都能在其自身約束條件規定的截止時間前執行完成，則判定該任務可調度，否則不可調度；如果某分區中的所有任務均可調度，則判定分區可調度，否則不可調度。

通過AADL Inspector的時間分析工具對所構建模型的動態行為進行仿真，可獲得分區任務調度甘特圖，仿真結果如圖13所示。

圖13 分區任務調度仿真甘特圖

圖13中，橫軸為系統運行時間，每格為5 ms。第1行表示處理器工作狀態，灰色部分表明其正在工作，其余為空閑。第2行和第5行分別表示分區1和分區2所獲得的處理器時間片，以灰色部分表示，由圖中可知分區1獲得時間片為20 ms，分區2獲得時間片為10 ms。第3行、第4行、第6行、第7行分別表示分區中的4個任務的執行情況，灰色表明任務處于等待執行狀態，黑色表明任務正在執行。

由于分區1的調度策略為DMS，任務的優先級與其截止時間成反比，則根據表2中參數，任務“Order”的優先級高于“Temperature_capture”，所以仿真結果中“Order”優先獲得處理器時間片，待其執行完成(3 ms)后，“Temperature_capture”才能執行，而在其完成(2 ms)后系統暫無任務執行，處于空閑狀態。另外，由于“Temperature_capture”的調度周期為15 ms，在分區1所獲得的1個處理器時間片下其將執行2次。

分區2采用的調度策略為RMS，任務的優先級與其周期成反比，則根據表2中參數，任務“Receiver”的優先級高于“Printer”，其余結論與分區1相同。

由圖13給出的分區調度仿真結果可知，所有任務均可調度，故所有分區均可調度，則可判定該IMA分區系統滿足可調度性要求。

為進一步驗證本文方法的有效性，對表2中給出的分區參數進行修改，并再次驗證系統的可調度性。

(1) 將分區1和分區2在一個主時鐘框架下獲得的處理器時間片分別改為30 ms和0 ms。此時由于分區2沒有分配處理器時間，其中的任務將無法在截止時間前完成。仿真結果如圖14所示。

圖14 修改分區時間片后的仿真結果

由圖14可知，分區1占用了全部的處理器時間片，其下的兩個任務均能夠按照時間約束條件正常執行，分區1滿足可調度性。然而，由于分區2無法獲得處理器時間片，其下的任務無法按照時間約束條件執行，仿真結果中出現了不可調度錯誤，在第6行、第7行以深灰色表示，提示分區2中的任務不可調度。由此可判定該IMA系統分區架構不滿足可調度性，這是由于分區時間片配置不合理導致的，仿真結果與上述分析結論相符。

(2) 將任務“Order”的執行時間修改為22 ms。此時，該任務的執行時間超過了其所規定的截止時間(8 ms)，同時也超過了分區1所獲得的處理器時間片(20 ms)。這不僅會導致該任務無法在規定截止時間前完成，也會對分區1內的另一任務的調度執行產生影響。仿真結果如圖15所示。

圖15 修改任務執行時間后的仿真結果

圖15中分區1下的兩個任務所在行出現了不可調度錯誤，表明分區1不滿足可調度性。其中，任務“Order”出現調度錯誤的時間點為其開始執行后的8 ms處，這是因為其未能在規定截止時間前完成執行。任務“Temperature_capture”在0～20 ms時間段內出現調度錯誤的時間點為15 ms，這是因為其未能在再次被調度前完成上次調度的執行。另外，分區2及其下任務所在行未出現錯誤，說明其滿足可調度性。仿真結果說明該IMA系統分區架構不滿足可調度性，這是由于任務時間約束條件配置不合理導致的，仿真結果與上述分析結論相符。

通過上述驗證過程可知，本文所提出的基于體系結構模型的IMA分區可調度性驗證方法與實際相符，具備有效性。另外，由于只需一次性建模即可完成可調度性驗證，與現有方法相比，在驗證過程中避免了對AADL模型進行繁瑣的二次轉化。

5 結 語

本文以IMA系統軟件分區架構為研究對象，提出了一種基于體系結構模型的分區可調度性驗證方法。在建立IMA分區調度的主要概念與AADL語義映射規則的基礎上，通過AADL標準建模組件和行為附件分別構建IMA系統分區架構模型和分區調度策略模型，并基于所建模型調用AADL Inspector工具，通過模型分析的方法對IMA系統軟件分區可調度性進行驗證。通過驗證，可以及時發現分區調度配置中的錯誤，為保證系統安全性和可靠性提供方法支持。