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

?

基于MARTE的IMA系統(tǒng)時間資源可調(diào)度配置驗證

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

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

【關(guān)鍵詞】綜合航電系統(tǒng)；模型驅(qū)動工程；MARTE；系統(tǒng)資源配置

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

1　基于MARTE的IMA系統(tǒng)建模

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

1.1通信虛擬鏈路建模

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

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

1.2AFDX終端建模

AFDX終端系統(tǒng)提供設(shè)備到AFDX網(wǎng)絡的通信接入口，負責完成從分區(qū)或者設(shè)備中下發(fā)的通信任務并進行數(shù)據(jù)收發(fā)。終端系統(tǒng)根據(jù)通信需求和通信鏈路中的數(shù)據(jù)幀大小來設(shè)置相關(guān)的系統(tǒng)參數(shù)，包括終端最大數(shù)據(jù)幀長和最小包間隙等參數(shù)。MARTE中的CommunicationEndPoint(CE P)組件表示通信元素通過CM進行傳輸?shù)慕涌冢⑶抑话粋€屬性packetSize，和CM組件中的elementSize屬性相匹配。因此用MARTE中的CEP組件來表示AFDX終端，用CEP組件中的packetSize屬性表示終端與通信鏈路相匹配的數(shù)據(jù)幀大小參數(shù)。

1.3分區(qū)建模

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

1.4進程建模

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

2　IMA系統(tǒng)時間資源配置驗證框架

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

圖1　IMA系統(tǒng)可調(diào)度性驗證框架

3　驗證實例分析

表1描述了系統(tǒng)應用分區(qū)（Papp）和系統(tǒng)分區(qū)（Psys）在總時間框架（10ms）下的分區(qū)間和分區(qū)內(nèi)任務集的調(diào)度情況，調(diào)度策略分別為EDF和DMS，分配的時間片大小分別為6和4，每個分區(qū)內(nèi)都包含有任務，周期，執(zhí)行時間和截止時間等任務集參數(shù)。

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

圖2　分區(qū)任務調(diào)度甘特仿真圖及可調(diào)性分析結(jié)果

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

參考文獻

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

[2]胡軍,馬金晶,程楨,等.模型驅(qū)動的安全關(guān)鍵系統(tǒng)重配置信息驗證方法研究[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－），男，南京航空航天大學碩士研究生，研究方向為軟件分析與驗證。

作者簡介：