基于MARTE的IMA系統時間資源可調度配置驗證

南京航空航天大學計算機科學與技術學院 程　楨

?

基于MARTE的IMA系統時間資源可調度配置驗證

南京航空航天大學計算機科學與技術學院 程楨

【摘要】目前綜合模塊化航空電子系統（IMA）在資源配置方面有非常高的安全可靠性需求，其中時間資源的可調度性配置驗證也顯得至關重要。本文在AFDX網絡架構下提出了一種IMA系統時間相關概念的MARTE建模和時間資源可調度配置的正確性驗證方法。建立了IMA系統通信虛擬鏈路、AFDX終端、分區以及進程等相關元素到MARTE模型元素的建模規則，并設計了基于可調度分析工具MAST的時間資源可調度配置驗證框架，最后利用相關實例進行仿真和分析得到驗證結果。

【關鍵詞】綜合航電系統；模型驅動工程；MARTE；系統資源配置

隨著航空領域系統日益復雜的發展趨勢，綜合模塊化航空電子系統（Integrated Modular Avionics, IMA）[1]已廣泛應用于機載航空電子系統。資源共享是IMA系統典型的特征，如何確保IMA系統開發過程中時間資源配置的安全性顯得至關重要，也成為近年來航空電子系統工程領域的一個重要挑戰。文獻[2]主要基于單個IMA系統對資源的配置文件信息進行建模轉換與驗證，沒有考慮實際情況中的AFDX網絡，文獻[3]給出了如何在任務時間需求函數的基礎上去計算系統所消耗的時間,并得出了系統可調度性的判定定理。文獻[4]詳細介紹了本文所利用的MARTE建模語言。本文從時間資源驗證角度，提出了一種AFDX網絡架構下IMA系統的建模方法以及時間資源驗證框架，基于模型驅動的方法對時間資源的可調度性進行了正確性驗證。

1　基于MARTE的IMA系統建模

在IMA資源配置過程中，若要對時間資源分配進行可調度性驗證，首先需要將系統的實時行為與時間約束轉換為MARTE模型來描述。本文主要對其中與時間行為和約束相關的通信虛擬鏈路、AFDX終端、分區、進程等核心概念展開建模方法的研究。

1.1通信虛擬鏈路建模

虛擬鏈路（Virtual Link）是由AFDX網絡中進行通信的終端節點之間建立起來的邏輯鏈路，具有帶寬資源隔離功能，通常由一到多個子鏈路構成。虛擬鏈路的帶寬資源主要通過數據幀長度、帶寬分配間隙、數據傳輸模式等參數設置得到保證。MARTE中的CommunicationMedia(CM)組件可以表示源終端和目的終端之間的數據傳輸，因此用CM組件中的elementSize屬性可以表示虛擬鏈路中的數據幀長度，用CM組件中的capacity屬性和elementSize屬性來表示虛擬鏈路中的帶寬分配間隙參數，用CM組件中的transmMode屬性

表示數據傳輸模式，主要有三種傳輸模式分別為：simplex, half-duplex和full-duplex。

1.2AFDX終端建模

AFDX終端系統提供設備到AFDX網絡的通信接入口，負責完成從分區或者設備中下發的通信任務并進行數據收發。終端系統根據通信需求和通信鏈路中的數據幀大小來設置相關的系統參數，包括終端最大數據幀長和最小包間隙等參數。MARTE中的CommunicationEndPoint(CE P)組件表示通信元素通過CM進行傳輸的接口，并且只包含一個屬性packetSize，和CM組件中的elementSize屬性相匹配。因此用MARTE中的CEP組件來表示AFDX終端，用CEP組件中的packetSize屬性表示終端與通信鏈路相匹配的數據幀大小參數。

1.3分區建模

IMA系統IPM中的分區是IMA系統中的一個核心概念，它要求在時間和空間上的隔離性，保證每個軟件在自己的分區中運行，且不同分區任務的運行互相不受影響。在IPM資源配置階段，分區被調度的周期和運行時間均按照需求配置好，且不同分區的地址空間也由內存管理分配好。MARTE中的swSchedulingResource(SR)和ProcessingResource(PR)組件共同構建了一個邏輯資源來指明系統運行時資源的分配情況（任務調度，分區資源等），每個邏輯資源可以用來表明調度信息和內存分配等情況。因此可用SR和PR組件來表示IMA系統中的分區概念。SR組件指明分區內的任務調度信息，SR中的schedulers屬性指明分區調度策略相關信息，同時PR組件指明了分區中的任務集。

1.4進程建模

分區中的進程是系統執行主體，包含了執行代碼，執行數據以及堆棧區域等資源。多個進程運行在某個分區中，分區通過指明進程的調度策略，搶占策略，內存分配情況，最大響應時間等信息來控制進程的執行，從而實現相應的應用功能?？梢杂肕ARTE中的SR組件表示分區中的進程概念，因為SR組件在MARTE中通過時間周期或外部事件來執行線程，是系統最基本的調度執行單元?？梢杂肧R組件的相應屬性來表示相應的任務集所包含的時間約束，包括任務的執行周期、是否可搶占、截止時間、優先級等。

2　IMA系統時間資源配置驗證框架

本文針對IMA系統時間資源配置驗證，提出了一種基于第三方工具MAST[5]仿真方法實現的可調度性判定方法。針對系統時間資源配置行為的MARTE模型和相關自定義調度策略，利用MAST工具作進一步可調度分析，得到可調度性判定結果和調度仿真甘特圖。具體方法框架如圖1所示，按照此驗證框架實例分析見下一章節描述。

圖1　IMA系統可調度性驗證框架

3　驗證實例分析

表1描述了系統應用分區（Papp）和系統分區（Psys）在總時間框架（10ms）下的分區間和分區內任務集的調度情況，調度策略分別為EDF和DMS，分配的時間片大小分別為6和4，每個分區內都包含有任務，周期，執行時間和截止時間等任務集參數。

根據上文描述得到系統的MARTE模型后，作為MAST工具的輸入得到相應的文本文件，并可加入相關時間約束等自定義調度策略。最后通過MAST工具集中的調度分析工具得到可調度性判定結果，包括任務在仿真時長內的調度甘特圖以及判定結果如圖2所示。

圖2　分區任務調度甘特仿真圖及可調性分析結果

圖2中左部分為MAST工具顯示的時間資源配置的可調度性分析結果，由圖可知按照表1中的時間資源配置系統的時間資源是滿足需求的且不會發生某個分區或進程得不到調度的情況；圖中右部分為調度仿真甘特圖分析，由圖可知按照實例中的時間配置情況，4個進程任務均得到調度且不會發生窗口重疊等情況，時間資源的配置都驗證通過。實例表明，本文所描述的模型驅動的方法可以用來對IMA系統時間資源的配置做正確性驗證工作。

參考文獻

[1]Parr G R,Edwards R.Integrated modular avionics[J].Air & Space Europe,1999,1(2):72-75.

[2]胡軍,馬金晶,程楨,等.模型驅動的安全關鍵系統重配置信息驗證方法研究[J].計算機科學與探索,2015,9(4):385-402.

[3]He Feng,Song Liru,Xiong HuaGang.Two level task partition scheduling design in integrated modular avionics.Journal of Beijing University of Aeronautics and Astronautics,2008,34 (11):1364-1368.

[4]Omg U. Profile for schedulability, performance, and time specification[J].Object Management Group,2003.

[5]Pasaje J L M,Harbour M G,Drake J M.Mast real-time view: A graphic uml tool for modeling object-oriented real-time systems[C]. In:Real-Time Systems Symposium,2001.(RTSS 2001). Proceedings.22nd IEEE.IEEE,2001.245-256.

程楨（1990－），男，南京航空航天大學碩士研究生，研究方向為軟件分析與驗證。

作者簡介：