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

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

?

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

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

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

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

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

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

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

1.1通信虛擬鏈路建模

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

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

1.2AFDX終端建模

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

1.3分區(qū)建模

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

1.4進(jìn)程建模

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

2　IMA系統(tǒng)時(shí)間資源配置驗(yàn)證框架

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

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

3　驗(yàn)證實(shí)例分析

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

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

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

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

參考文獻(xiàn)

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

[2]胡軍,馬金晶,程楨,等.模型驅(qū)動(dòng)的安全關(guān)鍵系統(tǒng)重配置信息驗(yàn)證方法研究[J].計(jì)算機(jī)科學(xué)與探索,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－），男，南京航空航天大學(xué)碩士研究生，研究方向?yàn)檐浖治雠c驗(yàn)證。

作者簡(jiǎn)介：