王明明，胡 軍，張維珺，李宛倩

(南京航空航天大學(xué) 計算機(jī)科學(xué)與技術(shù)學(xué)院，江蘇 南京 211106)

1 概 述

飛機(jī)機(jī)載系統(tǒng)歷經(jīng)幾代的發(fā)展，經(jīng)歷了分立式航電、聯(lián)合式航電系統(tǒng)和綜合模塊化航空電子系統(tǒng)(integrated modular avionics,IMA)[1-2]，機(jī)載航空電子系統(tǒng)現(xiàn)已廣泛采用IMA。在IMA系統(tǒng)中，多個實時應(yīng)用以時間/空間多分區(qū)的形式在計算平臺上同時運(yùn)行，有效提升了系統(tǒng)的功能、性能、可靠性和可維護(hù)性，同時降低了開發(fā)、維護(hù)和升級的支出。資源的共享是IMA系統(tǒng)的重要特征，或者說是IMA系統(tǒng)的核心功能，只有讓資源有效合理的共享，才能合理分配和使用航電系統(tǒng)的資源。在綜合航電系統(tǒng)開發(fā)過程中，對其中各個子系統(tǒng)和組件進(jìn)行合理高效的資源分配并確保資源配置的安全性尤為重要。

IMA系統(tǒng)資源配置是綜合航電系統(tǒng)整個開發(fā)過程中至關(guān)重要的一個環(huán)節(jié)，如何確保已分配的資源滿足系統(tǒng)需求是系統(tǒng)能夠安全正確運(yùn)行的必要條件。由于IMA系統(tǒng)的資源共享特性，IMA系統(tǒng)結(jié)構(gòu)是由多個硬件單元通過AFDX(avionics full duplex switched Ethernet,全雙工交換式以太網(wǎng))連接起來[3]，因此考慮網(wǎng)絡(luò)層次的資源配置驗證對系統(tǒng)完備性的提升有很大必要。文中從時間資源驗證角度，考慮分配各AFDX連接的IPM(integrated processing module，綜合處理模塊)資源時，根據(jù)需求給運(yùn)行在IPM上的多個應(yīng)用程序分配CPU時間，由于IMA系統(tǒng)分區(qū)具有分區(qū)間調(diào)度和分區(qū)內(nèi)調(diào)度的兩級調(diào)度特性，因此確保所有分區(qū)的調(diào)度時間滿足應(yīng)用程序需求以及分區(qū)內(nèi)的所有任務(wù)滿足調(diào)度時間約束是文中的主要研究內(nèi)容。

模型驅(qū)動工程(model driven engineering,MDE)是一種以建模(modeling)和模型轉(zhuǎn)換(model transformation)為主要途徑的軟件開發(fā)方法，是近年來出現(xiàn)在系統(tǒng)工程和軟件工程領(lǐng)域中的主流方法，其基本思想是以系統(tǒng)模型設(shè)計、模型轉(zhuǎn)換與分析/驗證為工程的重要核心，提高對復(fù)雜工程系統(tǒng)開發(fā)與維護(hù)的能力和效率[4-6]?；谀Ｐ偷南到y(tǒng)開發(fā)和形式化方法的要求[7-9]也已經(jīng)在最新版本的航空軟件適航標(biāo)準(zhǔn)DO-178C中正式提出。MARTE(modeling and analysis of real-time and embedded systems，實時嵌入式系統(tǒng)建模與分析)支持對復(fù)雜嵌入式系統(tǒng)設(shè)計中所需的功能建模以及廣泛存在的時間約束、資源分配等非功能屬性的建模與分析，是目前工業(yè)界已經(jīng)得到應(yīng)用的一類專門針對復(fù)雜實時嵌入式系統(tǒng)設(shè)計與分析的規(guī)范，應(yīng)用MARTE的實時特性對系統(tǒng)時間行為進(jìn)行建模描述將有助于對系統(tǒng)時間資源需求方面的驗證[10-11]。

根據(jù)IMA系統(tǒng)資源配置過程中對系統(tǒng)時間資源的分配，確保系統(tǒng)分區(qū)內(nèi)的任務(wù)能夠滿足調(diào)度時間約束要求，采用基于模型驅(qū)動的方法對AFDX網(wǎng)絡(luò)下IMA系統(tǒng)進(jìn)行建模并采用第三方工具進(jìn)行可調(diào)度性分析來驗證CPU時間資源配置的正確性。

2 相關(guān)背景知識

2.1 IMA網(wǎng)絡(luò)體系結(jié)構(gòu)概述

本節(jié)主要從IMA系統(tǒng)資源方面闡述IMA體系結(jié)構(gòu)，整個系統(tǒng)網(wǎng)絡(luò)架構(gòu)由IPM、AFDX交換機(jī)、AFDX終端系統(tǒng)、遠(yuǎn)程數(shù)據(jù)集中器(remote data collector，RDC)等組成[12]，各設(shè)備模塊之間通過航空電子通信網(wǎng)絡(luò)實現(xiàn)數(shù)據(jù)通信。

IPM是計算資源提供者，為駐留在IPM中的應(yīng)用分區(qū)提供計算資源，包括內(nèi)存和調(diào)度時間；AFDX交換機(jī)提供消息轉(zhuǎn)發(fā)等功能，多個交換機(jī)互聯(lián)形成一個AFDX網(wǎng)絡(luò)；AFDX終端提供用于將設(shè)備接入到AFDX網(wǎng)絡(luò)的接口；RDC設(shè)備負(fù)責(zé)收集信息和發(fā)送經(jīng)過處理的信息。

2.2 MARTE Profile

MARTE是OMG于2007年底發(fā)布的新UML Profile，用來取代原有的針對調(diào)度、性能和時間的UML Profile SPT[13]。MARTE不僅能夠?qū)?fù)雜嵌入式實時系統(tǒng)中軟硬件等層面的功能性和非功能性方面進(jìn)行有效建模，同時與UML2.0標(biāo)準(zhǔn)和MDA兼容，其作為UML推薦的實時和嵌入式系統(tǒng)建模的正式規(guī)范，目前已被工業(yè)界認(rèn)可并使用。MARTE中主要包含有基礎(chǔ)模型包、設(shè)計模型包和分析模型包，分別封裝的包括基礎(chǔ)(foundation)、建模(modeling)和分析(analyzing)3個部分。

2.3 MAST-2模型

MAST(modeling and analysis suite for real-time applications，實時系統(tǒng)建模與分析套件)是一套用于實時應(yīng)用建模與調(diào)度性分析的開源工具，提供了時間需求建模、分析等工具[14]。MAST工具集的核心是MAST模型，通過分析實時系統(tǒng)應(yīng)用的時間行為來作為MAST工具輸入。目前MAST模型包含MAST-1和MAST-2兩種模型，模型格式主要為文本格式或XML格式，其中MAST-2是在MAST-1模型的基礎(chǔ)上增加了AFDX網(wǎng)絡(luò)支持等功能，因此文中主要使用MAST-2模型來描述系統(tǒng)的時間行為。根據(jù)MAST規(guī)范，MAST-2模型可通過MARTE模型標(biāo)準(zhǔn)進(jìn)行圖形化描述，MAST_Model表示整個實時系統(tǒng)行為的MAST模型描述，包括全局屬性模型名稱和時間等；MAST-2模型包含了多個模型元素，其中Processing_Resource用來描述一個硬件組件的處理能力，包括執(zhí)行一段代碼或轉(zhuǎn)發(fā)一組消息等;Scheduler模型元素通過采用適當(dāng)?shù)恼{(diào)度策略來管理分配到處理器上的應(yīng)用或任務(wù);Schedulable _Resource模型元素描述了一個可調(diào)度實體，如處理器中一個執(zhí)行的任務(wù)或者網(wǎng)絡(luò)中的通信任務(wù);Operation模型元素描述某個計算任務(wù)或者消息傳送的執(zhí)行能力范圍，包括任務(wù)執(zhí)行時間范圍和傳送消息大小范圍;End_To_End_Flow模型元素描述了系統(tǒng)中執(zhí)行的活動在一系列事件觸發(fā)條件下相互之間的聯(lián)系，其中包括外部事件External_Events、內(nèi)部事件Internal_Events(包含時間需求)以及事件處理器Event_Handlers三種類型。

3 IMA系統(tǒng)資源配置與MARTE建模

3.1 IMA系統(tǒng)資源配置流程框架

將某飛機(jī)級功能集成到IMA平臺之前，需要根據(jù)該功能需求和IMA平臺提供的資源功能域?qū)ο到y(tǒng)進(jìn)行資源的有效配置。圖1給出了一個IMA資源配置流程框架，包括配置過程中必要的資源配置驗證，使得整個配置方法是一個循環(huán)迭代的過程，第4節(jié)將詳細(xì)給出針對IPM處理器時間調(diào)度資源分配的驗證方法。

圖1 IMA系統(tǒng)資源配置流程

IMA資源配置過程為：

(1)配置準(zhǔn)備:在IMA資源配置工作前需要設(shè)置一些應(yīng)用在整個工程配置中的通用參數(shù)、屬性和約束等，例如系統(tǒng)可用資源域、電源總線等。

(2)獲取系統(tǒng)駐留功能需求(host function requirement,HFRQ)和資源域需求:根據(jù)對需要集成到IMA平臺上的飛機(jī)級功能的分析，獲取具體的計算資源、I/O資源、通信資源等需求，同時包括安全性需求，再根據(jù)系統(tǒng)宿主功能需求所要求的資源，獲取所需系統(tǒng)資源需求(如IPM、RDC、AFDX等資源)，可將需求定義形成指定格式配置文件(如XML)，在今后工作中方便解析配置文件重新獲取需求。

(3)IMA資源計算:根據(jù)HFRQ和資源域計算IMA系統(tǒng)配置所需的資源數(shù)量。

(4)生成IMA網(wǎng)絡(luò)架構(gòu)圖：根據(jù)HFRQ和資源域以及資源的初步計算，形成系統(tǒng)網(wǎng)絡(luò)架構(gòu)圖，并根據(jù)需求將系統(tǒng)資源組件通過總線進(jìn)行連接。

(5)資源分配：根據(jù)HFRQ和資源域進(jìn)行系統(tǒng)資源(包括計算資源、IO資源、通信資源)的分配。

(6)形成配置文件：資源配置完成后形成配置文件，并對配置文件進(jìn)行分析與驗證。

在資源配置過程中需要進(jìn)行必要的驗證工作，整個配置方法是一個循環(huán)迭代不斷修正的過程，因此拓?fù)鋱D產(chǎn)生后需要進(jìn)行資源的重新計算、資源分配后需要進(jìn)行資源的重新計算和網(wǎng)絡(luò)架構(gòu)圖的重新生成等，其中對IPM時間資源的配置驗證是文中的主要工作，對于其他如IO資源、通信資源以及IPM內(nèi)存資源的配置驗證將在后續(xù)工作中展開。

3.2 使用MARTE對IMA系統(tǒng)進(jìn)行建模

在配置IMA系統(tǒng)資源時，若想驗證分配的可調(diào)度性，需要使用MARTE對系統(tǒng)的時間及其約束等進(jìn)行建模。文中從網(wǎng)絡(luò)架構(gòu)層面，暫不考慮AFDX交換機(jī)內(nèi)部復(fù)雜結(jié)構(gòu)，針對IMA系統(tǒng)中的網(wǎng)絡(luò)通信和計算資源，對其中虛擬鏈路、AFDX終端、資源設(shè)備模塊、分區(qū)、進(jìn)程等進(jìn)行建模并分析。

3.2.1 虛擬鏈路建模

虛擬鏈路是一條邏輯線路，連接AFDX網(wǎng)絡(luò)中相互通信的兩個終端。虛擬鏈路具有隔離帶寬資源的功能?？梢允褂肕ARTE內(nèi)部的CM組件表示相互通信的兩個終端之間的數(shù)據(jù)傳輸，數(shù)據(jù)幀的長度可以用其中的elementSize屬性值來表示，帶寬的分配間隙參數(shù)可以用此組件內(nèi)部的capacity屬性和elementSize屬性來表示，數(shù)據(jù)傳輸模式可以用該組件內(nèi)部的transmMode屬性來表示。

3.2.2 AFDX終端建模

AFDX終端是AFDX網(wǎng)絡(luò)與外部設(shè)備之間進(jìn)行通信的接口，執(zhí)行設(shè)備或者從分區(qū)發(fā)出的通信任務(wù)，并且發(fā)送和轉(zhuǎn)發(fā)數(shù)據(jù)。AFDX終端系統(tǒng)通過設(shè)置系統(tǒng)的相關(guān)參數(shù)來滿足系統(tǒng)的通信需求，這些參數(shù)包括最小包間隙和終端最大數(shù)據(jù)幀長等?？梢允褂肅EP組件表示AFDX終端，AFDX終端與通信鏈路之間傳輸?shù)臄?shù)據(jù)幀大小參數(shù)可以用該組件中的packetSize屬性表示。

3.2.3 資源設(shè)備模塊建模

IMA系統(tǒng)中的資源設(shè)備模塊包括核心處理模塊IPM、遠(yuǎn)程數(shù)據(jù)集中器RDC、AFDX交換機(jī)以及控制器等,每個模塊內(nèi)部都有自己獨(dú)立的處理單元來執(zhí)行相應(yīng)的功能。其中IPM為駐留在分區(qū)中的應(yīng)用提供計算資源，AFDX交換機(jī)提供通信資源，用來提供消息轉(zhuǎn)發(fā)功能，RDC作為航電系統(tǒng)輸入輸出設(shè)備負(fù)責(zé)收集數(shù)據(jù)并對數(shù)據(jù)進(jìn)行封裝。在MARTE內(nèi)，可以用hwProcessor組件表示系統(tǒng)的執(zhí)行環(huán)境，hwProcessor組件可以用來對IMA中IPM模塊概念進(jìn)行建模，模塊名可用description屬性來定義，分區(qū)之間的調(diào)度策略的建?？梢杂胔wProcessor組件的mainScheduler中的schedPolicy值來表示。同時MARTE中的hwProcessor組件和HwDevice組件可表示AFDX交換機(jī)、RDC等資源模塊概念。

3.2.4 分區(qū)建模

分區(qū)(partition)的重要設(shè)計思想就是隔離性，每個進(jìn)程只能在其所在的分區(qū)里執(zhí)行，且各個分區(qū)內(nèi)部的任務(wù)的執(zhí)行是獨(dú)立的。隔離性包括時間和空間隔離性。MARTE的SR組件和PR組件可以用來表示系統(tǒng)運(yùn)行時資源的分配情況。所以用這兩個組件來表示分區(qū)。分區(qū)內(nèi)的任務(wù)調(diào)度信息可以用SR組件來表示，分區(qū)調(diào)度方法相關(guān)信息可以表示為SR組件里的schedulers屬性，分區(qū)中的任務(wù)集也可以用PR組件來表示。

3.2.5 進(jìn)程建模

進(jìn)程(process)在分區(qū)內(nèi)，其中的資源包括代碼、數(shù)據(jù)和存儲區(qū)等。上節(jié)中提到的SR組件可以用來表示分區(qū)中進(jìn)程的概念。

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

在完成了IMA系統(tǒng)中資源配置相關(guān)信息的MARTE建模后，本節(jié)將基于MAST對系統(tǒng)進(jìn)行可調(diào)度性判定，以驗證時間資源配置的正確性。

4.1 IMA系統(tǒng)調(diào)度模型特征

在IMA系統(tǒng)的IPM模塊中包含有多個分區(qū)，各分區(qū)里面包含有其任務(wù)的集合。資源配置階段將處理器時間通過時間片來分配到每個分區(qū)，分區(qū)里的任務(wù)運(yùn)行分配的時間片(時間片包含偏移量(offset)和持續(xù)時間(duration)兩個參數(shù))，當(dāng)時間片用完時，在下一個時間片到來前暫停執(zhí)行操作。對應(yīng)各個分區(qū)之間和分區(qū)內(nèi)部的任務(wù)集合，此調(diào)度模型通過下面兩級調(diào)度策略來實現(xiàn)。

(1)分區(qū)間調(diào)度：該調(diào)度是在IPM資源配置時確定的，每個分區(qū)周期性地分配到時間片，時間片大小用duration表示。所有分區(qū)至少分配到一個分區(qū)窗口。分區(qū)間調(diào)度需要保證所有分區(qū)的時間片大小和周期以及主時間框架要滿足需求，且窗口不能重合。

(2)分區(qū)內(nèi)調(diào)度：分區(qū)內(nèi)調(diào)度根據(jù)對應(yīng)的任務(wù)調(diào)度策略來對任務(wù)進(jìn)程集進(jìn)行時間分配。在IPM資源配置階段是無法為每個任務(wù)具體分配到時間片的，所以無法直接判定每個任務(wù)獲得的時間片是否都滿足需求。這里需要用戶自定義調(diào)度策略，然后借助于MAST工具進(jìn)行可調(diào)度性的判定。

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

根據(jù)IMA系統(tǒng)分區(qū)調(diào)度特性，驗證IMA系統(tǒng)時間資源的配置，提出了一套仿真方法，該方法基于MAST工具，仿真判定IMA系統(tǒng)分區(qū)的可調(diào)度性。IMA系統(tǒng)可調(diào)度性驗證框架如圖2所示。

4.3 IMA系統(tǒng)的MAST-2模型描述

根據(jù)IMA系統(tǒng)的MARTE模型描述和相關(guān)時間需求約束可以建立MAST-2文本模型，用其作為MAST可調(diào)度性判定工具的輸入來分析系統(tǒng)的可調(diào)度性。MAST-2模型元素在第2.3節(jié)已經(jīng)介紹，下面將描述如何根據(jù)MARTE模型構(gòu)建相應(yīng)的MAST-2文本模型，從而描述IMA系統(tǒng)，主要從Processing_Resource、Scheduler、Scheduling_Resource、Operation、End_To_End_Flow等MAST-2模型元素來描述相關(guān)IMA系統(tǒng)的屬性。

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

Processing_Resource用來描述一個硬件組件的處理能力，包括執(zhí)行一段代碼或轉(zhuǎn)發(fā)一組消息等。Processing_Resource的子類型有Regular_Processor和AFDX_Link等，Regular_Processor描述處理器模塊執(zhí)行應(yīng)用程序的能力，AFDX_Link描述處理器或交換機(jī)之間采用AFDX協(xié)議傳輸消息的鏈路。所以MARTE模型中IPM模塊可以用Processing_Resource中的Regular_Processor類型表示，AFDX交換機(jī)網(wǎng)絡(luò)可以用AFDX_Link表示。

(1)Scheduler模型元素。

Scheduler模型元素通過采用適當(dāng)?shù)恼{(diào)度策略來管理分配到處理器上的應(yīng)用或任務(wù)，調(diào)度策略包含固定優(yōu)先級Fixed_Priority_Policy、最早截止時間優(yōu)先EDF等。Scheduler具有分層結(jié)構(gòu)，包含Primary_Scheduler和Secondary_Scheduler類型。

(2)Schedulable_Resource模型元素。

Schedulable_Resource模型元素描述了一個可調(diào)度實體，如處理器中一個執(zhí)行的任務(wù)或者網(wǎng)絡(luò)中的通信任務(wù)。Schedulable_Resource的子類型有Thread和Communication_Channel，Thread描述Regular_Processor模型中一個線程或者任務(wù)的執(zhí)行，Communication_Channel描述網(wǎng)絡(luò)中消息的傳輸。因此在IMA系統(tǒng)的MARTE模型中，每個進(jìn)程任務(wù)可以由Thread類型來描述。

(3)Operation模型元素。

Operation元素描述某個計算任務(wù)或者消息傳送的執(zhí)行需要的處理能力范圍，包括任務(wù)執(zhí)行時間范圍和傳送消息大小范圍。Operation的子類型包括Code_Operation和Message_Operation，分別描述計算任務(wù)和消息傳送的處理。

(4)End_To_End_Flow模型元素。

End_To_End_Flow模型元素描述了系統(tǒng)中執(zhí)行的活動在一系列事件觸發(fā)條件下相互之間的聯(lián)系，其中包括外部事件External_Events、內(nèi)部事件Internal_Events(包含時間需求)以及事件處理器Event_Handlers三種類型。

可將IMA分區(qū)間調(diào)度用End_To_End_Flow模型元素描述，各個分區(qū)的時間片設(shè)置在入口事件和結(jié)束事件之間，且分別擁有一個Hard global deadline表示分區(qū)可用的時間片。

5 驗證實例分析

基于第三節(jié)和第四節(jié)介紹的建模方法和時間資源分配的可調(diào)度性驗證框架，本節(jié)將具體給出IMA系統(tǒng)中機(jī)載水處理子系統(tǒng)(WaterAndWaste,WAW)的例子，介紹使用MARTE對WAW系統(tǒng)相關(guān)屬性進(jìn)行建模，并借助MAST工具將MARTE模型轉(zhuǎn)換成對應(yīng)的MAST-2模型，加入自定義調(diào)度策略并進(jìn)一步進(jìn)行調(diào)度仿真，根據(jù)返回結(jié)果判斷系統(tǒng)的可調(diào)度性。

根據(jù)航空規(guī)范ATA-38的描述，WAW系統(tǒng)主要功能是對飛機(jī)中的用水及污水進(jìn)行處理，包括存儲和傳輸清水、存儲和移除污水。圖3描述了WAW系統(tǒng)的硬件資源網(wǎng)絡(luò)結(jié)構(gòu)。根據(jù)IMA系統(tǒng)配置流程的介紹，該結(jié)構(gòu)是在確定HFRQ和資源域后進(jìn)行IMA估算、拓?fù)渖伞DC與交換機(jī)資源分配、IPM資源分配等流程后形成的。圖中包含2個信號控制器用來接受WAW系統(tǒng)中蓄水池的各種信號，并以模擬信號的形式傳遞給對應(yīng)的RDC；2個RDC與信號控制器和AFDX交換機(jī)相連進(jìn)行數(shù)字和模擬信號的轉(zhuǎn)換；2個AFDX交換機(jī)將各個設(shè)備連接到AFDX網(wǎng)絡(luò)；1個IPM包含1個應(yīng)用分區(qū)和1個系統(tǒng)分區(qū)，應(yīng)用分區(qū)根據(jù)接受到的數(shù)據(jù)計算當(dāng)前系統(tǒng)狀態(tài)，并發(fā)送控制命令信號，系統(tǒng)分區(qū)主要監(jiān)控錯誤信息等；以及各設(shè)備之間的通信虛擬鏈路。

圖3 機(jī)載水處理系統(tǒng)架構(gòu)

表1展示了WAW的分區(qū)調(diào)度信息。分區(qū)分為應(yīng)用分區(qū)(Papp)和系統(tǒng)分區(qū)(Psys)，調(diào)度策略分別為EDF(最早截止時間優(yōu)先)和DMS(截止時間單調(diào)調(diào)度算法)，分區(qū)下的任務(wù)集參數(shù)包括：周期、任務(wù)、執(zhí)行時間和截止時間等。

表1 WAW系統(tǒng)分區(qū)調(diào)度信息 ms

按照第三節(jié)對IMA系統(tǒng)轉(zhuǎn)化為MARTE模型的描述，可將WAW系統(tǒng)及其時間信息轉(zhuǎn)換為MARTE對應(yīng)組件描述，WAW系統(tǒng)對應(yīng)的MARTE模型中，用HwProcessor組件和HwDevice組件表示系統(tǒng)中的2個AFDX交換機(jī)、2個RDC遠(yuǎn)程數(shù)據(jù)收集器以及2個控制器，其中包含一些屬性參數(shù)；HwProcessor組件和MutualExclusionResource組件表示IPM處理器模塊，其下包含一個系統(tǒng)分區(qū)和一個應(yīng)用分區(qū)，分別用MARTE內(nèi)部的swSchedulingResource和ProcessingResource兩個組件以及該組件內(nèi)部的屬性的組合來表示，每個分區(qū)假設(shè)有兩個運(yùn)行的任務(wù)，用swSchedulingResource組件表示其調(diào)度屬性；最后每個任務(wù)對應(yīng)有時間約束信息，用MARTE中的TimeConstraint組件表示，包括任務(wù)運(yùn)行時間片、截止時間等時間信息。

得到WAW系統(tǒng)的MARTE模型后，根據(jù)4.3節(jié)描述的方法及給出的實例建立WAW系統(tǒng)對應(yīng)的MAST-2模型文本文件，并加入相關(guān)時間約束等自定義調(diào)度策略。圖4為MAST工具分析得出的甘特圖及分區(qū)可調(diào)性分析結(jié)果。

圖4 甘特圖及分區(qū)可調(diào)性分析結(jié)果

結(jié)果顯示四個進(jìn)程的甘特圖未發(fā)生沖突的情況，時間分區(qū)資源配置驗證通過。

在IMA系統(tǒng)資源配置過程中，若需要對時間資源進(jìn)行重新配置，如對實例中WAW系統(tǒng)需增加一個應(yīng)用分區(qū)Papp2，此時需要對分區(qū)Papp2分配時間片等時間資源，重新分配后的信息如表2所示。假設(shè)總時間框架保持10 ms未進(jìn)行配置，則在對Papp2進(jìn)行時間資源分配后，由于分區(qū)總時間片之和大于總時間框架，所以在進(jìn)行驗證工作之后返回的結(jié)果將是系統(tǒng)不可調(diào)度。

表2 WAW分區(qū)重配置調(diào)度信息 ms

通過文中介紹的時間資源配置驗證方法以及相關(guān)實例的分析，可以檢查IMA系統(tǒng)相關(guān)的資源配置是否滿足需求，從而避免發(fā)生錯誤而導(dǎo)致的災(zāi)難性結(jié)果，確保了系統(tǒng)安全可靠的運(yùn)行。

6 結(jié)束語

提出一種基于模型驅(qū)動的方法對IMA系統(tǒng)時間資源配置進(jìn)行驗證分析。首先，根據(jù)建模方法將IMA系統(tǒng)轉(zhuǎn)換為相應(yīng)的MARTE模型并加入時間約束來描述；其次，根據(jù)所得MARTE模型構(gòu)建對應(yīng)的MAST-2文本模型，并制定相應(yīng)的自定義調(diào)度策略作為MAST工具的輸入進(jìn)行分析；最后調(diào)用MAST可調(diào)度性分析工具對MAST-2文本模型進(jìn)行可調(diào)度性判定。通過可調(diào)度性驗證IMA系統(tǒng)時間資源配置，如果不正確可進(jìn)行資源的重配置和重判定，進(jìn)而提高系統(tǒng)的安全性和可靠性。

未來的研究工作主要包括兩個方面：第一，當(dāng)前的驗證工作主要針對IMA系統(tǒng)IPM資源分配過程中的時間資源分配，而整個資源配置過程還包括內(nèi)存分配、通信資源分配等，所以為確保整個資源配置過程的安全性和可靠性，將會對與其他資源配置相關(guān)如內(nèi)存分配的安全性等展開研究；第二，文中的實例分析對象為IMA系統(tǒng)中經(jīng)過簡化的機(jī)載水處理系統(tǒng)，未來的研究工作將針對IMA系統(tǒng)中其他復(fù)雜子系統(tǒng)乃至整個IMA系統(tǒng)本身進(jìn)行資源配置相關(guān)的安全性驗證工作，以提高整個系統(tǒng)在實際應(yīng)用中的可用性和工作效率。

參考文獻(xiàn):

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

[2] 褚文奎,張鳳鳴,樊曉光.綜合模塊化航空電子系統(tǒng)軟件體系結(jié)構(gòu)綜述[J].航空學(xué)報,2009,30(10):1912-1917.

[3] ALENA R L,OSSENFORT J P,LAWS K I,et al.Communications for integrated modular avionics[C]//Aerospace conference.[s.l.]:IEEE,2007:1-18.

[4] SCHMIDT D C.Guest editor's introduction:model-driven engineering[J].Computer,2006,39(2):25-31.

[5] HUTCHINSON J,ROUNCEFIELD M,WHITTLE J.Model-driven engineering practices in industry[C]//33rd international conference on software engineering.[s.l.]:IEEE,2011:633-642.

[6] 胡 軍,馬金晶,劉 雪,等.模型驅(qū)動的安全關(guān)鍵系統(tǒng)重配置信息驗證方法[J].計算機(jī)科學(xué)與探索,2015,9(4):385-402.

[7] RIERSON L.Developing safety-critical software:a practical guide for aviation software and DO-178c compliance[M].[s.l.]:CRC Press,2013.

[8] RUSHBY J.New challenges in certification for aircraft software[C]//Proceedings of the ninth ACM international conference on embedded software.New York,NY,USA:ACM,2011:211-218.

[9] MOY Y,LEDINOT E,DELSENY H,et al.Testing or formal verification:Do-178c alternatives and industrial experience[J].IEEE Software,2013,30(3):50-57.

[10] 張 天,Frédéric JOUAULT,Christian ATTIOGBE,等.基于MDE的異構(gòu)模型轉(zhuǎn)換:從MARTE模型到FIACRE模型[J].軟件學(xué)報,2009,20(2):214-233.

[11] NARDONE R,MARRONE S.A model-driven methodology to evaluate performability of metro systems[J].Theory and Application of Multi-Formalism Modeling,2013，(1):259-270.

[12] LAUER M,ERMONT J,BONIOL F,et al.Latency and freshness analysis on IMA systems[C]//Emerging technologies & factory automation.[s.l.]:[s.n.],2011:1-8.

[13] MALLET F.CCSL:specifying clock constraints with UML/MARTE[J].Innovations in Systems & Software Engineering,2008,4(3):309-314.

[14] 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]//Real-time systems symposium.[s.l.]:[s.n.],2001:245-256.